Commit 2026-03-03 11:03 845535c7

View on Github →

feat(Data/Fintype/Order): add API for ciSup with finite indexing type (#35260) This PR adds API for indexed suprema/infima on ConditionallyCompleteLattices when the indexing type is finite. It also moves Finite.le_ciSup/Finite.ciInf_le to Mathlib.Data.Fintype.Order and golfs it. We use the new lemmas to golf a few proofs in Mathlib.

Estimated changes

added theorem Finite.ciInf_inf
added theorem Finite.ciInf_le
added theorem Finite.ciInf_le_of_le
added theorem Finite.ciInf_mono
added theorem Finite.ciSup_mono
added theorem Finite.ciSup_sup
added theorem Finite.le_ciSup
added theorem Finite.le_ciSup_of_le
deleted theorem Finite.ciInf_le
deleted theorem Finite.le_ciSup