[Merged by Bors] - feat(measure_theory/measure_space): add ae_imp_iff #6218
Conversation
RemyDegenne
added
easy
| @@ -305,6 +305,9 @@ instance : countable_Inter_filter μ.ae := | |||
| exact measure_Union_null (subtype.forall.2 hS) | |||
| end⟩ | |||
|
|
|||
| lemma ae_imp_iff {p : α → Prop} {q : Prop} : (∀ᵐ x ∂μ, q → p x) ↔ (q → ∀ᵐ x ∂μ, p x) := | |||
There was a problem hiding this comment.
Wouldn't it be better if the names matched? I.e., ae_imp_distrib_left? But I am not sure I get the point of the lemma: we have a whole interface for eventually, and we won't copy every lemma for ae (maybe just the most important ones). Is this a lemma you will use several times in the ae version?
There was a problem hiding this comment.
I had statements of the form "forall a, forall b, prop1 a -> prop2 b -> ae prop3 x", and wanted to get the almost everywhere out of all implications and forall. For the forall there is the lemma ae_all_iff, and I thought it strange that there was no similarly named lemma for the implications. I got the impression that those ae lemmas were here so that the user of measure.ae does not have to use filters.
But I also understand the point of not replicating everything and to only provide new lemmas in cases where for example countability is used.
There was a problem hiding this comment.
and there is already ae_ball_iff, which does something similar to what I wanted, but I could not get it to apply.
There was a problem hiding this comment.
The ae_* lemmas are here for historical reasons: they were there before filter.eventually was added to mathlib. You can directly apply lemmas about filter.eventually because ∀ᵐ a ∂ μ is a notation, not a definition.
|
ok, the fact that other similar lemmas for ae are already there is convincing. Choose the name you like most, and then you can merge. |
|
✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
This is `filter.eventually_imp_distrib_left` specialized to the measure.ae filter.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This is `filter.eventually_imp_distrib_left` specialized to the measure.ae filter.
YaelDillies
removed
the
awaiting-review
This is
filter.eventually_imp_distrib_leftspecialized to the measure.ae filter.