Commit 2023-05-13 21:44 bb17f9bb

View on Github →

fix: correct mathlib3-style lattice lemma names (#3957)

Estimated changes

Modified Mathlib/Data/ENat/Lattice.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem WithBot.csupᵢ_empty

added theorem WithBot.csupₛ_empty

deleted theorem WithBot.supᵢ_empty

deleted theorem WithBot.supₛ_empty

deleted theorem WithTop.supr_coe_eq_top

deleted theorem WithTop.supr_coe_lt_top

added theorem WithTop.supᵢ_coe_eq_top

added theorem WithTop.supᵢ_coe_lt_top

Modified Mathlib/Order/Height.lean