Commit 2025-03-20 00:11 6ab59854

View on Github →

feat(ENat): (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n (#23101) From my PhD (MiscYD)

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.eq_top_iff_forall_ge

added theorem ENat.eq_top_iff_forall_gt

deleted theorem ENat.eq_top_iff_forall_le

deleted theorem ENat.eq_top_iff_forall_lt

modified theorem ENat.eq_top_iff_forall_ne

added theorem ENat.forall_natCast_le_iff_le

Modified Mathlib/Data/Option/Basic.lean

added theorem Option.eq_none_iff_forall_some_ne

deleted theorem Option.forall_some_ne_iff_eq_none

Modified Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.eq_bot_iff_forall_le

added theorem WithBot.eq_bot_iff_forall_lt

added theorem WithBot.eq_bot_iff_forall_ne

deleted theorem WithBot.forall_le_iff_eq_bot

deleted theorem WithBot.forall_lt_iff_eq_bot

deleted theorem WithBot.forall_ne_iff_eq_bot

added theorem WithTop.eq_top_iff_forall_ge

added theorem WithTop.eq_top_iff_forall_gt

added theorem WithTop.eq_top_iff_forall_ne

added theorem WithTop.forall_coe_le_iff_le

deleted theorem WithTop.forall_ge_iff_eq_top

deleted theorem WithTop.forall_gt_iff_eq_top

deleted theorem WithTop.forall_ne_iff_eq_top

Modified Mathlib/RingTheory/DiscreteValuationRing/Basic.lean