Commit 2026-01-16 12:21 0fcc1954

View on Github →

feat(Order/Bounds/Basic): use to_dual - part 1 (#33760) This PR uses to_dual in the first half of Order/Bounds/Basic, and in Order/Bounds/Defs, and also tags Iio/Ioi and Iic/Ici. This dualization went quite smoothly. The lemma HasSubset.Subset.iscofinalfor has been renamed to use correct capitalization (so that the name can be translated automatically), and has been deprecated. A new definition defined in this PR is IsCoinitial as a dual to IsCofinal, because IsCoinitialFor already existed as a dual to IsCofinalFor.

Estimated changes

modified theorem BddAbove.mono
deleted theorem BddBelow.dual
deleted theorem BddBelow.exists_le
deleted theorem BddBelow.inter_of_left
deleted theorem BddBelow.inter_of_right
deleted theorem BddBelow.mono
deleted theorem BddBelow.union
modified theorem IsCofinalFor.of_subset
deleted theorem IsCoinitialFor.of_subset
deleted theorem IsGLB.bddBelow
deleted theorem IsGLB.dual
deleted theorem IsGLB.inter_Iic_of_mem
deleted theorem IsGLB.lowerBounds_eq
deleted theorem IsGLB.mono
deleted theorem IsGLB.union
deleted theorem IsGreatest.dual
deleted theorem IsGreatest.isLUB
deleted theorem IsGreatest.mono
deleted theorem IsGreatest.nonempty
deleted theorem IsGreatest.union
deleted theorem IsGreatest.upperBounds_eq
deleted theorem IsLeast.bddBelow
deleted theorem IsLeast.lt_iff
modified theorem bddAbove_preimage_ofDual
modified theorem bddAbove_preimage_toDual
modified theorem bddAbove_singleton
deleted theorem bddBelow_Ici
deleted theorem bddBelow_Ioi
deleted theorem bddBelow_def
deleted theorem bddBelow_preimage_ofDual
deleted theorem bddBelow_preimage_toDual
deleted theorem bddBelow_singleton
deleted theorem bddBelow_union
deleted theorem bot_mem_lowerBounds
deleted theorem exists_glb_Ioi
deleted theorem isGLB_Ici
deleted theorem isGLB_Ioi
deleted theorem isGLB_congr
deleted theorem isGLB_iff_le_iff
deleted theorem isGLB_singleton
deleted theorem isGreatest_Iic
modified theorem isGreatest_singleton
deleted theorem isGreatest_top_iff
deleted theorem isGreatest_union_iff
modified theorem isLUB_singleton
deleted theorem isLeast_singleton
deleted theorem le_glb_Ioi
deleted theorem le_isGLB_iff
deleted theorem lowerBounds_Ici
deleted theorem lowerBounds_Ioi
deleted theorem lowerBounds_mono
deleted theorem lowerBounds_mono_mem
deleted theorem lowerBounds_mono_set
deleted theorem lowerBounds_singleton
deleted theorem lowerBounds_union
deleted theorem mem_lowerBounds
deleted theorem not_bddBelow_iff'
deleted theorem not_bddBelow_iff
deleted def BddBelow
deleted def IsCoinitialFor
deleted def IsGLB
deleted def IsGreatest
deleted def lowerBounds
deleted def Set.Ici
deleted theorem Set.Ici_def
modified theorem Set.Iic_def
modified theorem Set.Iio_def
deleted def Set.Ioi
deleted theorem Set.Ioi_def
deleted theorem Set.mem_Ici
modified theorem Set.mem_Iic
modified theorem Set.mem_Iio
deleted theorem Set.mem_Ioi