Commit 2026-01-25 18:29 899a4337

View on Github →

feat(Order/UpperLower/Basic): use to_dual - part 1 (#33950)

Estimated changes

deleted theorem IsLowerSet.bot_mem
deleted theorem IsLowerSet.bot_notMem
deleted theorem IsLowerSet.compl
deleted theorem IsLowerSet.erase
deleted theorem IsLowerSet.image
deleted theorem IsLowerSet.inter
deleted theorem IsLowerSet.sdiff
deleted theorem IsLowerSet.total
deleted theorem IsLowerSet.union
deleted theorem IsUpperSet.bot_mem
deleted theorem isLowerSet_compl
deleted theorem isLowerSet_empty
deleted theorem isLowerSet_iInter
deleted theorem isLowerSet_iInter₂
deleted theorem isLowerSet_iUnion
deleted theorem isLowerSet_iUnion₂
deleted theorem isLowerSet_iff_forall_lt
deleted theorem isLowerSet_sInter
deleted theorem isLowerSet_sUnion
deleted theorem isLowerSet_univ