Commit 2022-12-24 08:58 ffed42dd

View on Github →

Port/Order.ConditionallyCompleteLattice.Basic (#1181)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem GaloisConnection.l_csupᵢ

added theorem GaloisConnection.l_csupᵢ_set

added theorem GaloisConnection.l_csupₛ'

added theorem GaloisConnection.l_csupₛ

added theorem GaloisConnection.u_cinfᵢ

added theorem GaloisConnection.u_cinfᵢ_set

added theorem GaloisConnection.u_cinfₛ'

added theorem GaloisConnection.u_cinfₛ

added theorem IsGLB.cinfᵢ_eq

added theorem IsGLB.cinfᵢ_set_eq

added theorem IsGLB.cinfₛ_eq

added theorem IsGreatest.csupₛ_eq

added theorem IsGreatest.csupₛ_mem

added theorem IsLUB.csupᵢ_eq

added theorem IsLUB.csupᵢ_set_eq

added theorem IsLUB.csupₛ_eq

added theorem IsLeast.cinfₛ_eq

added theorem IsLeast.cinfₛ_mem

added theorem Monotone.cinfₛ_image_le

added theorem Monotone.csupᵢ_mem_Inter_Icc_of_antitone

added theorem Monotone.csupₛ_image_le

added theorem Monotone.le_cinfₛ_image

added theorem Monotone.le_csupₛ_image

added theorem Monotone.map_cinfₛ

added theorem MonotoneOn.map_cinfₛ

added theorem OrderIso.map_cinfᵢ

added theorem OrderIso.map_cinfᵢ_set

added theorem OrderIso.map_cinfₛ'

added theorem OrderIso.map_cinfₛ

added theorem OrderIso.map_csupᵢ

added theorem OrderIso.map_csupᵢ_set

added theorem OrderIso.map_csupₛ'

added theorem OrderIso.map_csupₛ

added theorem WithBot.coe_infᵢ

added theorem WithBot.coe_infₛ'

added theorem WithBot.coe_supᵢ

added theorem WithBot.coe_supₛ'

added theorem WithBot.supᵢ_empty

added theorem WithBot.supₛ_empty

added theorem WithTop.coe_infᵢ

added theorem WithTop.coe_infₛ'

added theorem WithTop.coe_infₛ

added theorem WithTop.coe_supᵢ

added theorem WithTop.coe_supₛ'

added theorem WithTop.coe_supₛ

added theorem WithTop.infᵢ_empty

added theorem WithTop.infₛ_empty

added theorem WithTop.is_glb_infₛ'

added theorem WithTop.is_glb_infₛ

added theorem WithTop.is_lub_supₛ'

added theorem WithTop.is_lub_supₛ

added theorem WithTop.supr_coe_eq_top

added theorem WithTop.supr_coe_lt_top

added theorem cinfᵢ_const

added theorem cinfᵢ_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem cinfᵢ_le'

added theorem cinfᵢ_le

added theorem cinfᵢ_le_of_le

added theorem cinfᵢ_mem

added theorem cinfᵢ_mono

added theorem cinfᵢ_pos

added theorem cinfᵢ_set_le

added theorem cinfᵢ_unique

added theorem cinfₛ_Icc

added theorem cinfₛ_Ici

added theorem cinfₛ_Ico

added theorem cinfₛ_Ioc

added theorem cinfₛ_Ioi

added theorem cinfₛ_Ioo

added theorem cinfₛ_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem cinfₛ_image2_eq_cinfₛ_cinfₛ

added theorem cinfₛ_image2_eq_cinfₛ_csupₛ

added theorem cinfₛ_image2_eq_csupₛ_cinfₛ

added theorem cinfₛ_image2_eq_csupₛ_csupₛ

added theorem cinfₛ_insert

added theorem cinfₛ_le'

added theorem cinfₛ_le

added theorem cinfₛ_le_cinfₛ'

added theorem cinfₛ_le_cinfₛ

added theorem cinfₛ_le_csupₛ

added theorem cinfₛ_le_iff

added theorem cinfₛ_le_of_le

added theorem cinfₛ_lt_of_lt

added theorem cinfₛ_mem

added theorem cinfₛ_pair

added theorem cinfₛ_singleton

added theorem cinfₛ_union

added theorem cinfₛ_univ

added theorem cinfₛ_upper_bounds_eq_csupₛ

added def conditionallyCompleteLatticeOfInf

added def conditionallyCompleteLatticeOfLatticeOfInf

added def conditionallyCompleteLatticeOfLatticeOfSup

added def conditionallyCompleteLatticeOfSup

added theorem csupᵢ_const

added theorem csupᵢ_eq_of_forall_le_of_forall_lt_exists_gt

added theorem csupᵢ_false

added theorem csupᵢ_le'

added theorem csupᵢ_le

added theorem csupᵢ_le_iff'

added theorem csupᵢ_le_iff

added theorem csupᵢ_mem_Inter_Icc_of_antitone_Icc

added theorem csupᵢ_mono'

added theorem csupᵢ_mono

added theorem csupᵢ_of_empty

added theorem csupᵢ_pos

added theorem csupᵢ_set_le_iff

added theorem csupᵢ_unique

added theorem csupₛ_Icc

added theorem csupₛ_Ico

added theorem csupₛ_Iic

added theorem csupₛ_Iio

added theorem csupₛ_Ioc

added theorem csupₛ_Ioo

added theorem csupₛ_empty

added theorem csupₛ_eq_of_forall_le_of_forall_lt_exists_gt

added theorem csupₛ_eq_of_is_forall_le_of_forall_le_imp_ge

added theorem csupₛ_image2_eq_cinfₛ_cinfₛ

added theorem csupₛ_image2_eq_cinfₛ_csupₛ

added theorem csupₛ_image2_eq_csupₛ_cinfₛ

added theorem csupₛ_image2_eq_csupₛ_csupₛ

added theorem csupₛ_insert

added theorem csupₛ_inter_le

added theorem csupₛ_le'

added theorem csupₛ_le

added theorem csupₛ_le_csupₛ

added theorem csupₛ_le_iff'

added theorem csupₛ_le_iff

added theorem csupₛ_lower_bounds_eq_cinfₛ

added theorem csupₛ_pair

added theorem csupₛ_singleton

added theorem csupₛ_union

added theorem exists_between_of_forall_le

added theorem exists_lt_of_cinfᵢ_lt

added theorem exists_lt_of_cinfₛ_lt

added theorem exists_lt_of_lt_csupᵢ'

added theorem exists_lt_of_lt_csupᵢ

added theorem exists_lt_of_lt_csupₛ'

added theorem exists_lt_of_lt_csupₛ

added theorem infₛ_eq_argmin_on

added theorem is_glb_cinfᵢ

added theorem is_glb_cinfᵢ_set

added theorem is_glb_cinfₛ

added theorem is_least_cinfₛ

added theorem is_lub_csupᵢ

added theorem is_lub_csupᵢ_set

added theorem is_lub_csupₛ'

added theorem is_lub_csupₛ

added theorem le_cinfᵢ

added theorem le_cinfᵢ_iff'

added theorem le_cinfᵢ_iff

added theorem le_cinfᵢ_set_iff

added theorem le_cinfₛ

added theorem le_cinfₛ_iff''

added theorem le_cinfₛ_iff'

added theorem le_cinfₛ_iff

added theorem le_cinfₛ_inter

added theorem le_csupᵢ

added theorem le_csupᵢ_iff'

added theorem le_csupᵢ_of_le

added theorem le_csupᵢ_set

added theorem le_csupₛ

added theorem le_csupₛ_iff'

added theorem le_csupₛ_iff

added theorem le_csupₛ_of_le

added theorem lt_csupₛ_of_lt

added theorem not_mem_of_csupₛ_lt

added theorem not_mem_of_lt_cinfₛ

added theorem subset_Icc_cinfₛ_csupₛ