Commit 2024-02-03 14:26 69f70a5a

View on Github →

chore: Rename Real.ciSup_empty (#10217) and a few more to clarify that they are about IsEmpty, not about ∅. Make a few more lemmas simp.`

Estimated changes

Modified Mathlib/Analysis/NormedSpace/PiLp.lean

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/Data/Nat/Lattice.lean

Modified Mathlib/Data/Real/Archimedean.lean

deleted theorem Real.ciInf_empty

deleted theorem Real.ciSup_empty

added theorem Real.iSup_of_isEmpty

modified theorem Real.sSup_univ

Modified Mathlib/Data/Real/NNReal.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/Order/CompleteLattice.lean

deleted theorem iInf_of_empty'

added theorem iInf_of_isEmpty