Commit 2024-06-30 23:36 454c4050

View on Github →

feat(Order/Interval/Set): trivial generalization of a lemma about UnorderedInterval (#14199)

Add uIoc_subset_uIcc
Relax the hypothesis of uIoc_of_lt from a < to a ≤ and change the name of the lemma to uIoc_of_ge
Fix dependencies

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

Modified Mathlib/MeasureTheory/Integral/IntervalAverage.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/Order/Interval/Set/OrderEmbedding.lean

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean

added theorem Set.uIoc_of_ge

deleted theorem Set.uIoc_of_lt

added theorem Set.uIoc_subset_uIcc