Commit 2026-08-16 12:22 e0c7e5b5

View on Github →

feat(Order/CompleteLattice/Basic): tag iSup_of_empty' with @[simp] (#38859) The theorem says iSup f = sSup ∅ when the domain of f is empty, and dually iInf f = sInf ∅.

Estimated changes

added theorem Real.iInf_of_isEmpty
modified theorem Real.iSup_of_isEmpty
modified theorem ENat.iInf_eq_natCast_iff
modified theorem ENat.iInf_eq_top_of_isEmpty
modified theorem NNReal.natCast_iInf
modified theorem WithBot.ciSup_empty
modified theorem WithTop.iInf_empty