Commit 2022-12-18 10:04 48505344

View on Github →

feat port: order.complete_lattice (#1053) aba57d4d3dae35460225919dcd82fe91355162f9 ~~Depends on #1040~~

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Group/Instances.lean

Modified Mathlib/Algebra/Order/Monoid/OrderDual.lean

Modified Mathlib/Order/Basic.lean

modified theorem OrderDual.Preorder.dual_dual

modified theorem OrderDual.linearOrder.dual_dual

Created Mathlib/Order/CompleteLattice.lean

added theorem Antitone.infᵢ_nat_add

added theorem Antitone.le_map_infᵢ

added theorem Antitone.le_map_infᵢ₂

added theorem Antitone.le_map_infₛ

added theorem Antitone.map_supᵢ_le

added theorem Antitone.map_supᵢ₂_le

added theorem Antitone.map_supₛ_le

added theorem Equiv.infᵢ_comp

added theorem Equiv.supᵢ_comp

added theorem Function.Surjective.infᵢ_comp

added theorem Function.Surjective.supᵢ_comp

added theorem IsGLB.infᵢ_eq

added theorem IsGLB.infₛ_eq

added theorem IsLUB.supᵢ_eq

added theorem IsLUB.supₛ_eq

added theorem Monotone.infᵢ_comp_eq

added theorem Monotone.le_map_supᵢ

added theorem Monotone.le_map_supᵢ₂

added theorem Monotone.le_map_supₛ

added theorem Monotone.map_infᵢ_le

added theorem Monotone.map_infᵢ₂_le

added theorem Monotone.map_infₛ_le

added theorem Monotone.supᵢ_comp_eq

added theorem Monotone.supᵢ_nat_add

added theorem OrderIso.map_infᵢ

added theorem OrderIso.map_infₛ

added theorem OrderIso.map_supᵢ

added theorem OrderIso.map_supₛ

added theorem binary_relation_infₛ_iff

added theorem binary_relation_supₛ_iff

added theorem binfᵢ_const

added theorem binfᵢ_inf

added theorem binfᵢ_mono

added theorem binfᵢ_prod

added theorem bsupᵢ_const

added theorem bsupᵢ_mono

added theorem bsupᵢ_prod

added theorem bsupᵢ_sup

added def completeLatticeOfCompleteSemilatticeInf

added def completeLatticeOfCompleteSemilatticeSup

added def completeLatticeOfInf

added def completeLatticeOfSup

added theorem disjoint_supₛ_left

added theorem disjoint_supₛ_right

added theorem eq_singleton_bot_of_supₛ_eq_bot_of_nonempty

added theorem eq_singleton_top_of_infₛ_eq_top_of_nonempty

added theorem inf_binfᵢ

added theorem inf_eq_infᵢ

added theorem inf_infᵢ

added theorem inf_infᵢ_nat_succ

added def infᵢ.unexpander

added def infᵢ

added theorem infᵢ_Prop_eq

added theorem infᵢ_and'

added theorem infᵢ_and

added theorem infᵢ_apply

added theorem infᵢ_bool_eq

added theorem infᵢ_comm

added theorem infᵢ_congr

added theorem infᵢ_congr_Prop

added theorem infᵢ_const

added theorem infᵢ_const_mono

added theorem infᵢ_dite

added theorem infᵢ_emptyset

added theorem infᵢ_eq_bot

added theorem infᵢ_eq_dif

added theorem infᵢ_eq_if

added theorem infᵢ_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem infᵢ_eq_top

added theorem infᵢ_exists

added theorem infᵢ_extend_top

added theorem infᵢ_false

added theorem infᵢ_ge_eq_infᵢ_nat_add

added theorem infᵢ_image

added theorem infᵢ_inf

added theorem infᵢ_inf_eq

added theorem infᵢ_infᵢ_eq_left

added theorem infᵢ_infᵢ_eq_right

added theorem infᵢ_insert

added theorem infᵢ_ite

added theorem infᵢ_le'

added theorem infᵢ_le

added theorem infᵢ_le_iff

added theorem infᵢ_le_infᵢ_of_subset

added theorem infᵢ_le_infᵢ₂

added theorem infᵢ_le_of_le

added theorem infᵢ_lt_iff

added theorem infᵢ_mono'

added theorem infᵢ_mono

added theorem infᵢ_nat_gt_zero_eq

added theorem infᵢ_ne_top_subtype

added theorem infᵢ_neg

added theorem infᵢ_of_empty'

added theorem infᵢ_of_empty

added theorem infᵢ_option

added theorem infᵢ_option_elim

added theorem infᵢ_or

added theorem infᵢ_pair

added theorem infᵢ_plift_down

added theorem infᵢ_plift_up

added theorem infᵢ_pos

added theorem infᵢ_prod

added theorem infᵢ_range'

added theorem infᵢ_range

added theorem infᵢ_sigma

added theorem infᵢ_singleton

added theorem infᵢ_split

added theorem infᵢ_split_single

added theorem infᵢ_subtype''

added theorem infᵢ_subtype'

added theorem infᵢ_subtype

added theorem infᵢ_sum

added theorem infᵢ_sup_infᵢ_le

added theorem infᵢ_supᵢ_ge_nat_add

added theorem infᵢ_top

added theorem infᵢ_true

added theorem infᵢ_union

added theorem infᵢ_univ

added theorem infᵢ₂_comm

added theorem infᵢ₂_eq_top

added theorem infᵢ₂_le

added theorem infᵢ₂_le_of_le

added theorem infᵢ₂_mono'

added theorem infᵢ₂_mono

added theorem infₛ_Prop_eq

added theorem infₛ_apply

added theorem infₛ_diff_singleton_top

added theorem infₛ_empty

added theorem infₛ_eq_bot

added theorem infₛ_eq_infᵢ'

added theorem infₛ_eq_infᵢ

added theorem infₛ_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem infₛ_eq_top

added theorem infₛ_image'

added theorem infₛ_image2

added theorem infₛ_image

added theorem infₛ_insert

added theorem infₛ_le

added theorem infₛ_le_iff

added theorem infₛ_le_infₛ

added theorem infₛ_le_infₛ_of_forall_exists_le

added theorem infₛ_le_infₛ_of_subset_insert_top

added theorem infₛ_le_of_le

added theorem infₛ_le_supₛ

added theorem infₛ_lt_iff

added theorem infₛ_pair

added theorem infₛ_range

added theorem infₛ_singleton

added theorem infₛ_sup_le_infᵢ_sup

added theorem infₛ_union

added theorem infₛ_univ

added theorem isGLB_binfᵢ

added theorem isGLB_infᵢ

added theorem isGLB_infₛ

added theorem isLUB_bsupᵢ

added theorem isLUB_supᵢ

added theorem isLUB_supₛ

added theorem le_infᵢ

added theorem le_infᵢ_comp

added theorem le_infᵢ_const

added theorem le_infᵢ_iff

added theorem le_infᵢ₂

added theorem le_infᵢ₂_iff

added theorem le_infₛ

added theorem le_infₛ_iff

added theorem le_infₛ_inter

added theorem le_supᵢ'

added theorem le_supᵢ

added theorem le_supᵢ_iff

added theorem le_supᵢ_inf_supᵢ

added theorem le_supᵢ_of_le

added theorem le_supᵢ₂

added theorem le_supᵢ₂_of_le

added theorem le_supₛ

added theorem le_supₛ_iff

added theorem le_supₛ_of_le

added theorem lt_infᵢ_iff

added theorem lt_supᵢ_iff

added theorem lt_supₛ_iff

added theorem monotone_infₛ_of_monotone

added theorem monotone_supₛ_of_monotone

added theorem of_dual_infᵢ

added theorem of_dual_infₛ

added theorem of_dual_supᵢ

added theorem of_dual_supₛ

added theorem sup_bsupᵢ

added theorem sup_eq_supᵢ

added theorem sup_infₛ_le_infᵢ_sup

added theorem sup_supᵢ

added theorem sup_supᵢ_nat_succ

added def supᵢ.unexpander

added def supᵢ

added theorem supᵢ_Prop_eq

added theorem supᵢ_and'

added theorem supᵢ_and

added theorem supᵢ_apply

added theorem supᵢ_bool_eq

added theorem supᵢ_bot

added theorem supᵢ_comm

added theorem supᵢ_comp_le

added theorem supᵢ_congr

added theorem supᵢ_congr_Prop

added theorem supᵢ_const

added theorem supᵢ_const_le

added theorem supᵢ_const_mono

added theorem supᵢ_dite

added theorem supᵢ_emptyset

added theorem supᵢ_eq_bot

added theorem supᵢ_eq_dif

added theorem supᵢ_eq_if

added theorem supᵢ_eq_of_forall_le_of_forall_lt_exists_gt

added theorem supᵢ_eq_top

added theorem supᵢ_exists

added theorem supᵢ_extend_bot

added theorem supᵢ_false

added theorem supᵢ_ge_eq_supᵢ_nat_add

added theorem supᵢ_image

added theorem supᵢ_inf_le_inf_supₛ

added theorem supᵢ_inf_le_supₛ_inf

added theorem supᵢ_infᵢ_ge_nat_add

added theorem supᵢ_infᵢ_le_infᵢ_supᵢ

added theorem supᵢ_insert

added theorem supᵢ_ite

added theorem supᵢ_le

added theorem supᵢ_le_iff

added theorem supᵢ_le_supᵢ_of_subset

added theorem supᵢ_lt_iff

added theorem supᵢ_mono'

added theorem supᵢ_mono

added theorem supᵢ_nat_gt_zero_eq

added theorem supᵢ_ne_bot_subtype

added theorem supᵢ_neg

added theorem supᵢ_of_empty'

added theorem supᵢ_of_empty

added theorem supᵢ_option

added theorem supᵢ_option_elim

added theorem supᵢ_or

added theorem supᵢ_pair

added theorem supᵢ_plift_down

added theorem supᵢ_plift_up

added theorem supᵢ_pos

added theorem supᵢ_prod

added theorem supᵢ_range'

added theorem supᵢ_range

added theorem supᵢ_sigma

added theorem supᵢ_singleton

added theorem supᵢ_split

added theorem supᵢ_split_single

added theorem supᵢ_subtype''

added theorem supᵢ_subtype'

added theorem supᵢ_subtype

added theorem supᵢ_sum

added theorem supᵢ_sup

added theorem supᵢ_sup_eq

added theorem supᵢ_supᵢ_eq_left

added theorem supᵢ_supᵢ_eq_right

added theorem supᵢ_true

added theorem supᵢ_union

added theorem supᵢ_univ

added theorem supᵢ₂_comm

added theorem supᵢ₂_eq_bot

added theorem supᵢ₂_le

added theorem supᵢ₂_le_iff

added theorem supᵢ₂_le_supᵢ

added theorem supᵢ₂_mono'

added theorem supᵢ₂_mono

added theorem supₛ_Prop_eq

added theorem supₛ_apply

added theorem supₛ_diff_singleton_bot

added theorem supₛ_empty

added theorem supₛ_eq_bot

added theorem supₛ_eq_of_forall_le_of_forall_lt_exists_gt

added theorem supₛ_eq_supᵢ'

added theorem supₛ_eq_supᵢ

added theorem supₛ_eq_top

added theorem supₛ_image'

added theorem supₛ_image2

added theorem supₛ_image

added theorem supₛ_insert

added theorem supₛ_inter_le

added theorem supₛ_le

added theorem supₛ_le_iff

added theorem supₛ_le_supₛ

added theorem supₛ_le_supₛ_of_forall_exists_le

added theorem supₛ_le_supₛ_of_subset_insert_bot

added theorem supₛ_pair

added theorem supₛ_range

added theorem supₛ_singleton

added theorem supₛ_union

added theorem supₛ_univ

added theorem to_dual_infᵢ

added theorem to_dual_infₛ

added theorem to_dual_supᵢ

added theorem to_dual_supₛ

added theorem unary_relation_infₛ_iff

added theorem unary_relation_supₛ_iff