Commit 2022-12-23 10:31 c4a53859

View on Github →

Initial file copy from mathport

Estimated changes

Created Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem GaloisConnection.l_cSup'

added theorem GaloisConnection.l_cSup

added theorem GaloisConnection.l_csupr

added theorem GaloisConnection.l_csupr_set

added theorem GaloisConnection.u_cInf'

added theorem GaloisConnection.u_cInf

added theorem GaloisConnection.u_cinfi

added theorem GaloisConnection.u_cinfi_set

added theorem Inf_eq_argmin_on

added theorem Inf_mem

added theorem IsGLB.cInf_eq

added theorem IsGLB.cinfi_eq

added theorem IsGLB.cinfi_set_eq

added theorem IsGreatest.Sup_mem

added theorem IsGreatest.cSup_eq

added theorem IsLUB.cSup_eq

added theorem IsLUB.csupr_eq

added theorem IsLUB.csupr_set_eq

added theorem IsLeast.Inf_mem

added theorem IsLeast.cInf_eq

added theorem Monotone.cInf_image_le

added theorem Monotone.cSup_image_le

added theorem Monotone.csupr_mem_Inter_Icc_of_antitone

added theorem Monotone.le_cInf_image

added theorem Monotone.le_cSup_image

added theorem Monotone.map_Inf

added theorem MonotoneOn.map_Inf

added theorem OrderIso.map_cInf'

added theorem OrderIso.map_cInf

added theorem OrderIso.map_cSup'

added theorem OrderIso.map_cSup

added theorem OrderIso.map_cinfi

added theorem OrderIso.map_cinfi_set

added theorem OrderIso.map_csupr

added theorem OrderIso.map_csupr_set

added theorem WithBot.cSup_empty

added theorem WithBot.coe_Inf'

added theorem WithBot.coe_Sup'

added theorem WithBot.coe_infi

added theorem WithBot.coe_supr

added theorem WithBot.csupr_empty

added theorem WithTop.cInf_empty

added theorem WithTop.cinfi_empty

added theorem WithTop.coe_Inf'

added theorem WithTop.coe_Inf

added theorem WithTop.coe_Sup'

added theorem WithTop.coe_Sup

added theorem WithTop.coe_infi

added theorem WithTop.coe_supr

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_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_pair

added theorem cInf_singleton

added theorem cInf_union

added theorem cInf_univ

added theorem cInf_upper_bounds_eq_cSup

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 cinfi_const

added theorem cinfi_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem cinfi_le'

added theorem cinfi_le

added theorem cinfi_le_of_le

added theorem cinfi_mono

added theorem cinfi_pos

added theorem cinfi_set_le

added def conditionallyCompleteLatticeOfInf

added def conditionallyCompleteLatticeOfLatticeOfInf

added def conditionallyCompleteLatticeOfLatticeOfSup

added def conditionallyCompleteLatticeOfSup

added theorem csupr_const

added theorem csupr_eq_of_forall_le_of_forall_lt_exists_gt

added theorem csupr_false

added theorem csupr_le'

added theorem csupr_le

added theorem csupr_le_iff'

added theorem csupr_le_iff

added theorem csupr_mem_Inter_Icc_of_antitone_Icc

added theorem csupr_mono'

added theorem csupr_mono

added theorem csupr_of_empty

added theorem csupr_pos

added theorem csupr_set_le_iff

added theorem exists_between_of_forall_le

added theorem exists_lt_of_cInf_lt

added theorem exists_lt_of_cinfi_lt

added theorem exists_lt_of_lt_cSup'

added theorem exists_lt_of_lt_cSup

added theorem exists_lt_of_lt_csupr'

added theorem exists_lt_of_lt_csupr

added theorem infi_mem

added theorem infi_unique

added theorem is_glb_cInf

added theorem is_glb_cinfi

added theorem is_glb_cinfi_set

added theorem is_least_Inf

added theorem is_lub_cSup'

added theorem is_lub_cSup

added theorem is_lub_csupr

added theorem is_lub_csupr_set

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_iff

added theorem le_cSup_of_le

added theorem le_cinfi

added theorem le_cinfi_iff'

added theorem le_cinfi_iff

added theorem le_cinfi_set_iff

added theorem le_csupr

added theorem le_csupr_iff'

added theorem le_csupr_of_le

added theorem le_csupr_set

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

added theorem supr_unique