Commit 2024-11-08 18:13 42277c6a

View on Github →

feat(ENat): iSup_add (#15344) From the Carleson project

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

added theorem WithTop.addLECancellable_iff_ne_top

added theorem WithTop.addLECancellable_of_lt_top

added theorem WithTop.addLECancellable_of_ne_top

Modified Mathlib/Algebra/Order/Sub/WithTop.lean

added theorem WithTop.sub_ne_top_iff

Modified Mathlib/Data/ENNReal/Inv.lean

added theorem ENNReal.iSup_zero

deleted theorem ENNReal.iSup_zero_eq_zero

Modified Mathlib/Data/ENNReal/Operations.lean

added theorem ENNReal.sub_ne_top_iff

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.addLECancellable_of_lt_top

added theorem ENat.addLECancellable_of_ne_top

modified theorem ENat.add_one_eq_coe_top_iff

added theorem ENat.add_one_natCast_le_withTop_of_lt

deleted theorem ENat.add_one_nat_le_withTop_of_lt

added theorem ENat.natCast_ne_coe_top

deleted theorem ENat.nat_ne_coe_top

modified theorem ENat.one_le_iff_ne_zero_withTop

added theorem ENat.sub_eq_top_iff

added theorem ENat.sub_ne_top_iff

Created Mathlib/Data/ENat/BigOperators.lean

added theorem ENat.sum_iSup

added theorem ENat.sum_iSup_of_monotone

Modified Mathlib/Data/ENat/Lattice.lean

added theorem ENat.add_biSup'

added theorem ENat.add_biSup

added theorem ENat.add_iSup

added theorem ENat.add_sSup

added theorem ENat.biSup_add'

added theorem ENat.biSup_add

added theorem ENat.biSup_add_biSup_le'

added theorem ENat.biSup_add_biSup_le

added theorem ENat.iSup_add

added theorem ENat.iSup_add_iSup

added theorem ENat.iSup_add_iSup_le

added theorem ENat.iSup_add_iSup_of_monotone

modified theorem ENat.iSup_eq_zero

added theorem ENat.iSup_natCast

added theorem ENat.iSup_zero

added theorem ENat.sSup_add

added theorem ENat.sub_iSup

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Topology/Instances/ENat.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDimension.lean

Modified scripts/no_lints_prime_decls.txt