Commit 2025-03-11 23:04 2d1e2d7c

View on Github →

feat(Data/ENat): add eq_top_iff_forall_ne and similar lemmas (#21473)

Add eq_top_iff_forall_ne, eq_top_iff_forall_lt, eq_top_iff_forall_le
Simplify proof of exists_nat_gt
Rename variable in ne_top_iff_exists in order to align it with nerby lemmas

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.eq_top_iff_forall_le

added theorem ENat.eq_top_iff_forall_lt

added theorem ENat.eq_top_iff_forall_ne

modified theorem ENat.ne_top_iff_exists