Commit 2024-01-16 04:25 0b934338

View on Github →

chore(Fintype/Order): generalize Fintype to Finite in Directed lemmas (#9754)

Estimated changes

added theorem Directed.finite_le
added theorem Directed.finite_set_le
deleted theorem Directed.fintype_le
added theorem Finite.bddAbove_range
added theorem Finite.bddBelow_range
added theorem Finite.exists_ge
added theorem Finite.exists_le
deleted theorem Fintype.bddAbove_range
deleted theorem Fintype.bddBelow_range
deleted theorem Fintype.exists_ge
deleted theorem Fintype.exists_le
added theorem Set.Finite.exists_ge
added theorem Set.Finite.exists_le