Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Abstract measure
The 'almost everywhere' relation
relae
Next ⟩
brae
Metamath Proof Explorer
Ascii
Unicode
Theorem
relae
Description:
'almost everywhere' is a relation.
(Contributed by
Thierry Arnoux
, 20-Oct-2017)
Ref
Expression
Assertion
relae
⊢
Rel
⁡
ae
Proof
Step
Hyp
Ref
Expression
1
df-ae
⊢
ae
=
a
m
|
m
⁡
⋃
dom
⁡
m
∖
a
=
0
2
1
relopabi
⊢
Rel
⁡
ae