Theorem Set.infinite_of_forall_exists_lt

Modification history

2025-05-14 10:52

Mathlib/Data/Set/Finite/Basic.lean

refactor: spell results using `Minimal`/`MinimalFor` (#23487) …

Modified Set.infinite_of_forall_exists_lt View on Github →

2023-04-28 14:30

Mathlib/Data/Set/Finite.lean

feat: Lemmas relating definitions of infinite sets (#3672) …

Added Set.infinite_of_forall_exists_lt View on Github →