Commit 2024-06-11 23:44 d19a0ceb

View on Github →

chore: fix junk value for sInf on WithTop (#13717) As pointed out in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Definition.20of.20.60WithTop.2EinstInfSet.60/near/443609808, the current choice of junk value for sInf s when s : Set (WithTop α) is not bounded below does not coincide with sInf ∅. This makes it impossible to get a ConditionallyCompleteLinearOrder structure on WithTop α as we require the junk values to coincide. This PR fixes the choice of junk value for sInf s when s : Set (WithTop α) is not bounded below, making it equal to ⊤ = sInf ∅.

Estimated changes

modified theorem ENNReal.coe_sInf
modified theorem ENat.coe_iInf
modified theorem ENat.coe_sInf
modified theorem WithBot.ciSup_empty
modified theorem WithBot.coe_iInf
modified theorem WithBot.coe_iSup
modified theorem WithBot.coe_sInf'
modified theorem WithBot.coe_sSup'
deleted theorem WithBot.csSup_empty
modified theorem WithBot.sInf_eq
added theorem WithBot.sSup_empty
modified theorem WithBot.sSup_eq
modified theorem WithTop.coe_iInf
modified theorem WithTop.coe_iSup
modified theorem WithTop.coe_sInf'
modified theorem WithTop.coe_sInf
modified theorem WithTop.coe_sSup'
modified theorem WithTop.iInf_empty
modified theorem WithTop.sInf_empty
modified theorem WithTop.sInf_eq
modified theorem WithTop.sSup_eq