-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(data/set/finite): add lemmas relating definitions of infinite sets #18617
feat(data/set/finite): add lemmas relating definitions of infinite sets #18617
Conversation
Includes the following lemmas * `infinite.exists_nat_lt`, * `arb_large_infinite` * `infinite_iff_arb_large` Which state the following ```lean lemma infinite.exists_nat_lt {s : set ℕ} (hs : s.infinite) (n : ℕ) : ∃ m ∈ s, n < m lemma arb_large_infinite {S : set ℕ} : S.infinite → ∀ (n : ℕ ), ∃ (m : ℕ), (m ∈ S ∧ m > n) lemma infinite_iff_arb_large {S : set ℕ } : S.infinite ↔ (∀ (n : ℕ ), ∃ (m : ℕ), (m ∈ S ∧ m > n)) ```
lemma arb_large_infinite {S : set ℕ} : S.infinite → ∀ (n : ℕ ), ∃ (m : ℕ), (m ∈ S ∧ m > n) := | ||
begin | ||
intros h n, | ||
apply bex_def.mp, | ||
apply set.infinite.exists_nat_lt h, | ||
end |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This lemma is pretty much identical to infinite.exists_nat_lt
, so I don't think it's worth having.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
After removing arb_large_infinite
, could I then replace the definition of infinite_iff_arb_large
with the following?
lemma infinite_iff_arb_large {S : set ℕ } : S.infinite ↔ ∀ (n : ℕ ), ∃ (m : ℕ), (m ∈ S ∧ n < m) :=
begin
split,
{ intro hS,
have exists_nat_lt := hS.exists_nat_lt,
finish, },
{ exact infinite_exists_nat_lt, }
end
apply set.infinite.exists_nat_lt h, | ||
end | ||
|
||
lemma infinite_exists_nat_lt {S : set ℕ} : (∀ (n : ℕ ), ∃ (m : ℕ), (m ∈ S ∧ m > n)) → S.infinite := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this would be a better name and statement
lemma infinite_exists_nat_lt {S : set ℕ} : (∀ (n : ℕ ), ∃ (m : ℕ), (m ∈ S ∧ m > n)) → S.infinite := | |
lemma infinite_of_forall_exists_nat_lt {S : set ℕ} (h : ∀ n, ∃ m ∈ s, n < m) : S.infinite := |
Oh, I'm afraid our CI doesn't run on forks. You'll need to ask on Zulip for permission to push directly to a branch in our repository, and then reopen this PR. |
Sure, will do. Thank you! |
Add lemmas relating definitions of infinite sets
Includes the following lemmas
infinite.exists_nat_lt
,arb_large_infinite
infinite_iff_arb_large
Which state the following