Commit 2026-08-18 15:22 c82deec9

View on Github →

feat(Data/Fintype/Order): add Finite.ciInf_le_iff and friends (#42623) This PR adds Finite.ciInf_le_iff : ⨅ i, f i ≤ a ↔ ∃ x, f x ≤ a and friends.

Estimated changes

Modified Mathlib/Data/Fintype/Order.lean

added theorem Finite.ciSup_lt_iff

added theorem Finite.le_ciSup_iff

Modified Mathlib/Order/Bounds/Basic.lean

added theorem IsGreatest.le_iff

Modified Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

added theorem Finite.ciSup_mem

added theorem Finite.isGreatest_ciSup

added theorem Set.Nonempty.isGreatest_csSup

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

deleted theorem isGLB_ciInf

deleted theorem isGLB_ciInf_set