Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-24 15:26 1d94b2ea

View on Github →

refactor(order/conditionally_complete_lattice): split file (#17695)

Estimated changes

Modified src/algebra/bounds.lean

Modified src/algebra/order/nonneg/ring.lean

Modified src/algebra/support.lean

Modified src/algebra/tropical/big_operators.lean

Modified src/algebra/tropical/lattice.lean

Modified src/data/int/conditionally_complete_order.lean

Modified src/data/nat/lattice.lean

Modified src/data/real/basic.lean

Modified src/data/real/nnreal.lean

Modified src/data/set/intervals/monotone.lean

Modified src/measure_theory/measurable_space_def.lean

Modified src/order/complete_lattice_intervals.lean

Renamed src/order/conditionally_complete_lattice.lean to src/order/conditionally_complete_lattice/basic.lean

deleted theorem csupr_mul_csupr_le

deleted theorem csupr_mul_le

deleted theorem finset.inf'_eq_cInf_image

deleted theorem finset.inf'_id_eq_cInf

deleted theorem finset.nonempty.cInf_eq_min'

deleted theorem finset.nonempty.cInf_mem

deleted theorem finset.nonempty.cSup_eq_max'

deleted theorem finset.nonempty.cSup_mem

deleted theorem finset.nonempty.sup'_eq_cSup_image

deleted theorem finset.nonempty.sup'_id_eq_cSup

deleted theorem finset.sup'_eq_cSup_image

deleted theorem finset.sup'_id_eq_cSup

deleted theorem le_cinfi_mul

deleted theorem le_cinfi_mul_cinfi

deleted theorem le_mul_cinfi

deleted theorem mul_csupr_le

deleted theorem set.finite.cSup_lt_iff

deleted theorem set.finite.lt_cInf_iff

deleted theorem set.nonempty.cInf_mem

deleted theorem set.nonempty.cSup_mem

Created src/order/conditionally_complete_lattice/finset.lean

added theorem finset.inf'_eq_cInf_image

added theorem finset.inf'_id_eq_cInf

added theorem finset.nonempty.cInf_eq_min'

added theorem finset.nonempty.cInf_mem

added theorem finset.nonempty.cSup_eq_max'

added theorem finset.nonempty.cSup_mem

added theorem finset.nonempty.sup'_eq_cSup_image

added theorem finset.nonempty.sup'_id_eq_cSup

added theorem finset.sup'_eq_cSup_image

added theorem finset.sup'_id_eq_cSup

added theorem set.finite.cSup_lt_iff

added theorem set.finite.lt_cInf_iff

added theorem set.nonempty.cInf_mem

added theorem set.nonempty.cSup_mem

Created src/order/conditionally_complete_lattice/group.lean

added theorem csupr_mul_csupr_le

added theorem csupr_mul_le

added theorem le_cinfi_mul

added theorem le_cinfi_mul_cinfi

added theorem le_mul_cinfi

added theorem mul_csupr_le

Modified src/order/copy.lean

Modified src/order/ord_continuous.lean

Modified src/order/semiconj_Sup.lean

Modified src/set_theory/cardinal/basic.lean