Commit 2023-04-28 14:30 7be61534

View on Github →

feat: Lemmas relating definitions of infinite sets (#3672) Match https://github.com/leanprover-community/mathlib/pull/18620

Estimated changes

Modified Mathlib/Data/Finset/LocallyFinite.lean

added theorem Set.Infinite.exists_gt

added theorem Set.Infinite.exists_lt

added theorem Set.Infinite.not_bddAbove

added theorem Set.Infinite.not_bddBelow

added theorem Set.infinite_iff_exists_gt

added theorem Set.infinite_iff_exists_lt

Modified Mathlib/Data/Nat/Lattice.lean

Modified Mathlib/Data/Set/Finite.lean

deleted theorem Set.Infinite.exists_nat_lt

added theorem Set.infinite_of_forall_exists_gt

added theorem Set.infinite_of_forall_exists_lt