Commit 2026-04-02 16:35 6a7332dd

View on Github →

feat(Data/ENat): add lemma ENat.iInf_eq_coe_iff (#34144)

Estimated changes

Modified Mathlib/Data/ENat/Lattice.lean

added theorem ENat.iInf_eq_coe_iff

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem csInf_eq_iff

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem ciInf_eq_iff