-
Notifications
You must be signed in to change notification settings - Fork 44
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
notation for ae_eq
#1079
Labels
question ❓
There is an unanswered question here
renaming/refactoring 🔧
This is about a renaming or refactoring in the library
Milestone
Comments
Sure. (Without the dots IMO) |
and what about if we need to make the measure explicit? |
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 |
affeldt-aist
added
the
renaming/refactoring 🔧
This is about a renaming or refactoring in the library
label
Jul 29, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
question ❓
There is an unanswered question here
renaming/refactoring 🔧
This is about a renaming or refactoring in the library
analysis/theories/lebesgue_integral.v
Line 41 in c8adb03
what about using a notation such as
or
=a.e.
?The text was updated successfully, but these errors were encountered: