Commit 2024-07-22 05:54 0a67e5a4

View on Github →

chore(LiminfLimsup): fix namespaces (#14995)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Order/LiminfLimsup.lean

added theorem CompleteLatticeHom.apply_liminf_iterate

added theorem CompleteLatticeHom.apply_limsup_iterate

deleted theorem Filter.CompleteLatticeHom.apply_liminf_iterate

deleted theorem Filter.CompleteLatticeHom.apply_limsup_iterate

deleted theorem Filter.InfHom.le_apply_bliminf

deleted theorem Filter.OrderIso.apply_bliminf

deleted theorem Filter.OrderIso.apply_blimsup

deleted theorem Filter.SupHom.apply_blimsup_le

added theorem OrderIso.apply_bliminf

added theorem OrderIso.apply_blimsup

added theorem sInfHom.le_apply_bliminf

added theorem sSupHom.apply_blimsup_le