Commit 2022-12-23 10:35 436cde88

View on Github →

Revert "Initial file copy from mathport" This reverts commit c4a53859992bfffb07f0dcb0879a9377b7fffdde.

Estimated changes

deleted theorem GaloisConnection.l_cSup'
deleted theorem GaloisConnection.l_cSup
deleted theorem GaloisConnection.l_csupr
deleted theorem GaloisConnection.u_cInf'
deleted theorem GaloisConnection.u_cInf
deleted theorem GaloisConnection.u_cinfi
deleted theorem Inf_eq_argmin_on
deleted theorem Inf_mem
deleted theorem IsGLB.cInf_eq
deleted theorem IsGLB.cinfi_eq
deleted theorem IsGLB.cinfi_set_eq
deleted theorem IsGreatest.Sup_mem
deleted theorem IsGreatest.cSup_eq
deleted theorem IsLUB.cSup_eq
deleted theorem IsLUB.csupr_eq
deleted theorem IsLUB.csupr_set_eq
deleted theorem IsLeast.Inf_mem
deleted theorem IsLeast.cInf_eq
deleted theorem Monotone.cInf_image_le
deleted theorem Monotone.cSup_image_le
deleted theorem Monotone.le_cInf_image
deleted theorem Monotone.le_cSup_image
deleted theorem Monotone.map_Inf
deleted theorem MonotoneOn.map_Inf
deleted theorem OrderIso.map_cInf'
deleted theorem OrderIso.map_cInf
deleted theorem OrderIso.map_cSup'
deleted theorem OrderIso.map_cSup
deleted theorem OrderIso.map_cinfi
deleted theorem OrderIso.map_cinfi_set
deleted theorem OrderIso.map_csupr
deleted theorem OrderIso.map_csupr_set
deleted theorem WithBot.cSup_empty
deleted theorem WithBot.coe_Inf'
deleted theorem WithBot.coe_Sup'
deleted theorem WithBot.coe_infi
deleted theorem WithBot.coe_supr
deleted theorem WithBot.csupr_empty
deleted theorem WithTop.cInf_empty
deleted theorem WithTop.cinfi_empty
deleted theorem WithTop.coe_Inf'
deleted theorem WithTop.coe_Inf
deleted theorem WithTop.coe_Sup'
deleted theorem WithTop.coe_Sup
deleted theorem WithTop.coe_infi
deleted theorem WithTop.coe_supr
deleted theorem WithTop.is_glb_Inf'
deleted theorem WithTop.is_glb_Inf
deleted theorem WithTop.is_lub_Sup'
deleted theorem WithTop.is_lub_Sup
deleted theorem WithTop.supr_coe_eq_top
deleted theorem WithTop.supr_coe_lt_top
deleted theorem cInf_Icc
deleted theorem cInf_Ici
deleted theorem cInf_Ico
deleted theorem cInf_Ioc
deleted theorem cInf_Ioi
deleted theorem cInf_Ioo
deleted theorem cInf_image2_eq_cInf_cInf
deleted theorem cInf_image2_eq_cInf_cSup
deleted theorem cInf_image2_eq_cSup_cInf
deleted theorem cInf_image2_eq_cSup_cSup
deleted theorem cInf_insert
deleted theorem cInf_le'
deleted theorem cInf_le
deleted theorem cInf_le_cInf'
deleted theorem cInf_le_cInf
deleted theorem cInf_le_cSup
deleted theorem cInf_le_iff
deleted theorem cInf_le_of_le
deleted theorem cInf_lt_of_lt
deleted theorem cInf_pair
deleted theorem cInf_singleton
deleted theorem cInf_union
deleted theorem cInf_univ
deleted theorem cInf_upper_bounds_eq_cSup
deleted theorem cSup_Icc
deleted theorem cSup_Ico
deleted theorem cSup_Iic
deleted theorem cSup_Iio
deleted theorem cSup_Ioc
deleted theorem cSup_Ioo
deleted theorem cSup_empty
deleted theorem cSup_image2_eq_cInf_cInf
deleted theorem cSup_image2_eq_cInf_cSup
deleted theorem cSup_image2_eq_cSup_cInf
deleted theorem cSup_image2_eq_cSup_cSup
deleted theorem cSup_insert
deleted theorem cSup_inter_le
deleted theorem cSup_le'
deleted theorem cSup_le
deleted theorem cSup_le_cSup
deleted theorem cSup_le_iff'
deleted theorem cSup_le_iff
deleted theorem cSup_lower_bounds_eq_cInf
deleted theorem cSup_pair
deleted theorem cSup_singleton
deleted theorem cSup_union
deleted theorem cinfi_const
deleted theorem cinfi_le'
deleted theorem cinfi_le
deleted theorem cinfi_le_of_le
deleted theorem cinfi_mono
deleted theorem cinfi_pos
deleted theorem cinfi_set_le
deleted theorem csupr_const
deleted theorem csupr_false
deleted theorem csupr_le'
deleted theorem csupr_le
deleted theorem csupr_le_iff'
deleted theorem csupr_le_iff
deleted theorem csupr_mono'
deleted theorem csupr_mono
deleted theorem csupr_of_empty
deleted theorem csupr_pos
deleted theorem csupr_set_le_iff
deleted theorem exists_lt_of_cInf_lt
deleted theorem exists_lt_of_cinfi_lt
deleted theorem exists_lt_of_lt_cSup'
deleted theorem exists_lt_of_lt_cSup
deleted theorem exists_lt_of_lt_csupr'
deleted theorem exists_lt_of_lt_csupr
deleted theorem infi_mem
deleted theorem infi_unique
deleted theorem is_glb_cInf
deleted theorem is_glb_cinfi
deleted theorem is_glb_cinfi_set
deleted theorem is_least_Inf
deleted theorem is_lub_cSup'
deleted theorem is_lub_cSup
deleted theorem is_lub_csupr
deleted theorem is_lub_csupr_set
deleted theorem le_cInf
deleted theorem le_cInf_iff''
deleted theorem le_cInf_iff'
deleted theorem le_cInf_iff
deleted theorem le_cInf_inter
deleted theorem le_cSup
deleted theorem le_cSup_iff'
deleted theorem le_cSup_iff
deleted theorem le_cSup_of_le
deleted theorem le_cinfi
deleted theorem le_cinfi_iff'
deleted theorem le_cinfi_iff
deleted theorem le_cinfi_set_iff
deleted theorem le_csupr
deleted theorem le_csupr_iff'
deleted theorem le_csupr_of_le
deleted theorem le_csupr_set
deleted theorem lt_cSup_of_lt
deleted theorem not_mem_of_cSup_lt
deleted theorem not_mem_of_lt_cInf
deleted theorem subset_Icc_cInf_cSup
deleted theorem supr_unique