Commit 2026-03-20 14:17 2a6a215c

View on Github →

chore: use @[to_dual] extensively in CompleteLattice (#35209) This PR adds @[to_dual] annotations extensively in CompleteLattice/Defs.lean and CompleteLattice/Basic.lean, auto-generating many dual theorems and deleting the hand-written versions.

  • depends on: #35208 🤖 Prepared with Claude Code

Estimated changes

deleted theorem Antitone.map_iSup_le
deleted theorem Antitone.map_sSup_le
deleted theorem Equiv.biInf_comp
deleted theorem Equiv.iInf_comp
deleted theorem IsGLB.iInf_eq
deleted theorem Monotone.iInf_comp_eq
deleted theorem Monotone.map_iInf_le
deleted theorem Monotone.map_sInf_le
deleted theorem OrderIso.map_iInf
deleted theorem OrderIso.map_iInfâ‚‚
deleted theorem OrderIso.map_sInf
deleted theorem Prod.fst_iInf
deleted theorem Prod.fst_sInf
deleted theorem Prod.iInf_mk
deleted theorem Prod.snd_iInf
deleted theorem Prod.snd_sInf
deleted theorem Prod.swap_iInf
deleted theorem Prod.swap_sInf
deleted theorem Set.BijOn.iInf_comp
deleted theorem Set.BijOn.iInf_congr
deleted theorem biInf_congr'
deleted theorem biInf_congr
deleted theorem biInf_const
deleted theorem biInf_ge_eq_iInf
deleted theorem biInf_ge_eq_inf
deleted theorem biInf_ge_eq_of_monotone
deleted theorem biInf_gt_eq_iInf
deleted theorem biInf_inf
deleted theorem biInf_le
deleted theorem biInf_le_eq_iInf
deleted theorem biInf_le_eq_inf
deleted theorem biInf_lt_eq_iInf
deleted theorem biInf_mono
deleted theorem biInf_prod'
deleted theorem biInf_prod
modified theorem biSup_ge_eq_iSup
deleted theorem biSup_ge_eq_of_antitone
modified theorem bot_lt_iSup
deleted theorem iInf_and'
deleted theorem iInf_and
deleted theorem iInf_apply
deleted theorem iInf_comm
deleted theorem iInf_congr
deleted theorem iInf_const
deleted theorem iInf_const_mono
deleted theorem iInf_dite
deleted theorem iInf_emptyset
deleted theorem iInf_eq_bot
deleted theorem iInf_eq_dif
deleted theorem iInf_eq_if
deleted theorem iInf_eq_top
deleted theorem iInf_exists
deleted theorem iInf_extend_top
deleted theorem iInf_false
deleted theorem iInf_iInf_eq_left
deleted theorem iInf_iInf_eq_right
deleted theorem iInf_image2
deleted theorem iInf_image
deleted theorem iInf_inf
deleted theorem iInf_inf_eq
deleted theorem iInf_insert
deleted theorem iInf_ite
deleted theorem iInf_le
deleted theorem iInf_le_iInf_of_subset
deleted theorem iInf_le_iInfâ‚‚
deleted theorem iInf_le_of_le
deleted theorem iInf_lt_top
deleted theorem iInf_mono'
deleted theorem iInf_mono
deleted theorem iInf_ne_top_subtype
deleted theorem iInf_neg
deleted theorem iInf_of_empty
deleted theorem iInf_option
deleted theorem iInf_option_elim
deleted theorem iInf_or
deleted theorem iInf_pair
deleted theorem iInf_plift_down
deleted theorem iInf_plift_up
deleted theorem iInf_pos
deleted theorem iInf_prod'
deleted theorem iInf_prod
deleted theorem iInf_psigma'
deleted theorem iInf_psigma
deleted theorem iInf_range'
deleted theorem iInf_range
deleted theorem iInf_sigma'
deleted theorem iInf_sigma
deleted theorem iInf_singleton
deleted theorem iInf_split
deleted theorem iInf_split_single
deleted theorem iInf_subtype''
deleted theorem iInf_subtype'
deleted theorem iInf_subtype
deleted theorem iInf_sum
deleted theorem iInf_top
deleted theorem iInf_true
deleted theorem iInf_ulift
deleted theorem iInf_union
deleted theorem iInf_unique
deleted theorem iInf_univ
deleted theorem iInfâ‚‚_comm
deleted theorem iInfâ‚‚_eq_bot
deleted theorem iInfâ‚‚_eq_top
deleted theorem iInfâ‚‚_le
deleted theorem iInfâ‚‚_le_of_le
deleted theorem iInfâ‚‚_mono'
deleted theorem iInfâ‚‚_mono
modified theorem iSup_ulift
deleted theorem inf_biInf
deleted theorem inf_iInf
deleted theorem isGLB_biInf
deleted theorem isGLB_iInf
deleted theorem le_iInf
deleted theorem le_iInf_comp
deleted theorem le_iInf_const
deleted theorem le_iInf_iff
deleted theorem le_iInfâ‚‚
deleted theorem le_iInfâ‚‚_iff
deleted theorem le_sInf_inter
deleted theorem lt_iInf_iff
deleted theorem sInf_apply
deleted theorem sInf_apply_eq_sInf_image
deleted theorem sInf_diff_singleton_top
deleted theorem sInf_empty
deleted theorem sInf_eq_iInf'
deleted theorem sInf_eq_iInf
deleted theorem sInf_eq_top
deleted theorem sInf_image2
deleted theorem sInf_image
deleted theorem sInf_insert
deleted theorem sInf_pair
deleted theorem sInf_prod
deleted theorem sInf_range
deleted theorem sInf_singleton
deleted theorem sInf_union
deleted theorem sInf_univ
deleted theorem sInf_upperBounds_eq_sSup
deleted theorem biInf_lt_iff
deleted theorem iInf_lt_iff
deleted theorem sInf_eq_bot
deleted theorem sInf_lt_iff