Commit 2023-01-19 14:03 02ee755f

View on Github →

feat: port Data.Fintype.Lattice (#1674)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Lattice.lean

added theorem Finite.exists_max

added theorem Finite.exists_min

added theorem Finset.fold_inf_univ

added theorem Finset.fold_sup_univ

added theorem Finset.inf_univ_eq_infᵢ

added theorem Finset.sup_univ_eq_supᵢ