notation for `ae_eq`

[affeldt-aist]

analysis/theories/lebesgue_integral.v

Line 41 in c8adb03

(* ae_eq D f g == f is equal to g almost everywhere *)

what about using a notation such as

Reserved Notation "x '=ae' y " (at level 60, format "x  '=ae'  y").

or =a.e. ?

[CohenCyril]

Sure. (Without the dots IMO)
We could also use
{ae, f =1 g}
(This notation has the advantage of being the composition of two generic notations)

[affeldt-aist]

and what about if we need to make the measure explicit? {ae[mu], f =1 g} ? (If we need to make both the measure and the support set explicit, then {ae mu, forall x, x \in D -> f x = g x} is good enough, no need for a notation)

[affeldt-aist]

Maybe we should have defined

Definition ae_eq f g := {ae mu, forall x, D x -> f x = g x}.

as

Definition ae_eq f g := {ae mu, f \_ D =1 g \_ D}.

instead