Commit 2026-03-21 08:07 d1feaddb

View on Github →

chore(Order/UpperLower/CompleteLattice): use to_dual (#36920) This PR tags declarations about UpperSet/LowerSet with to_dual.

Estimated changes

deleted def LowerSet.Simps.coe
deleted theorem LowerSet.carrier_eq_coe
deleted theorem LowerSet.coe_bot
deleted theorem LowerSet.coe_compl
deleted theorem LowerSet.coe_eq_empty
deleted theorem LowerSet.coe_eq_univ
deleted theorem LowerSet.coe_iInf
deleted theorem LowerSet.coe_iInf₂
deleted theorem LowerSet.coe_iSup
deleted theorem LowerSet.coe_iSup₂
deleted theorem LowerSet.coe_inf
deleted theorem LowerSet.coe_map
deleted theorem LowerSet.coe_mk
deleted theorem LowerSet.coe_nonempty
deleted theorem LowerSet.coe_sInf
deleted theorem LowerSet.coe_sSup
deleted theorem LowerSet.coe_ssubset_coe
deleted theorem LowerSet.coe_subset_coe
deleted theorem LowerSet.coe_sup
deleted theorem LowerSet.coe_top
deleted def LowerSet.compl
deleted theorem LowerSet.compl_iInf₂
deleted theorem LowerSet.compl_iSup₂
deleted theorem LowerSet.compl_le_compl
deleted theorem LowerSet.compl_map
deleted theorem LowerSet.disjoint_coe
deleted theorem LowerSet.ext
deleted def LowerSet.map
deleted theorem LowerSet.map_map
deleted theorem LowerSet.map_refl
deleted theorem LowerSet.mem_compl_iff
deleted theorem LowerSet.mem_iInf_iff
deleted theorem LowerSet.mem_iInf₂_iff
deleted theorem LowerSet.mem_iSup_iff
deleted theorem LowerSet.mem_iSup₂_iff
deleted theorem LowerSet.mem_inf_iff
deleted theorem LowerSet.mem_map
deleted theorem LowerSet.mem_mk
deleted theorem LowerSet.mem_sInf_iff
deleted theorem LowerSet.mem_sSup_iff
deleted theorem LowerSet.mem_sup_iff
deleted theorem LowerSet.mem_top
deleted theorem LowerSet.notMem_bot
deleted theorem LowerSet.symm_map
modified theorem UpperSet.coe_mk
modified theorem UpperSet.coe_nonempty
modified theorem UpperSet.coe_ssubset_coe
modified def UpperSet.compl
modified theorem UpperSet.compl_map
modified theorem UpperSet.mem_mk
modified def upperSetIsoLowerSet