## Stream: new members

### Topic: infinite_iff_arb_large

#### Sam Ezeh (Mar 18 2023 at 19:09):

Old PR: https://github.com/leanprover-community/mathlib/pull/18617
Discord: https://discord.com/channels/679792285910827018/707609591940382830/1086371258255556719
I'd like to ask for push permission for some lemmas, is this the right stream to discuss mathlib?

#### Notification Bot (Mar 18 2023 at 19:15):

This topic was moved here from #maths > infinite_iff_arb_large by Eric Wieser.

Thank you!

#### Eric Wieser (Mar 18 2023 at 19:17):

I've granted you (dignissimus) write access!

#### Yaël Dillies (Mar 18 2023 at 19:34):

Incidentally, #18604 is relevant.

#### Sam Ezeh (Mar 18 2023 at 22:11):

After rewriting the type declaration I got this

lemma infinite_of_forall_exists_nat_lt {S : set ℕ} (h : ∀ (n : ℕ), ∃ m ∈ S, n < m) : S.infinite  :=
begin
intro hS, -- Assume S finite
let S2 : finset ℕ := set.finite.to_finset hS,
have h2 : ∃ B, ∀n ∈ S2, n ≤ B,
{ use finset.sup S2 id,
intros,
apply finset.le_sup H }, -- Exists maximum
cases h2 with N hN, -- N is the maximum
cases h N with n hn, -- n is larger than the maximum
cases hn with hnS hnN, -- n is in S, n is larger than maximum
have h3 := (set.finite.mem_to_finset hS).mpr hnS,
have h4 := hN n,
simp at h4 h3,
have smaller_than_max := h4 h3,
sorry,
end

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, },
{ intro hS,
have exists_nat_lt :=  infinite_of_forall_exists_nat_lt,
finish,
exact S, },
end


#### Sam Ezeh (Mar 18 2023 at 22:11):

For the sorry I just need false from N < n and n <= n

#### Sam Ezeh (Mar 18 2023 at 22:12):

I was going to ask for style criticism, but I'm having an issue where lean doesn't terminate and consumes 4GB+ of memory. I run sam@samtop ~/Documents/git/mathlib (git)-[infinite-set-lemmas] % lean src/data/set/finite.lean

#### Eric Wieser (Mar 18 2023 at 22:15):

Did you run leanproject get-cache?

#### Eric Wieser (Mar 18 2023 at 22:15):

Your previous proof ought to work with very few modifications with my suggested statement

#### Sam Ezeh (Mar 18 2023 at 22:28):

leanproject get-cachee was what I needed

#### Sam Ezeh (Mar 18 2023 at 22:30):

I got confused with the different goals from the new statement and started the proof from the beginning

#### Sam Ezeh (Mar 18 2023 at 22:34):

Before, the proof was like this

lemma infinite_exists_nat_lt {S : set ℕ} : (∀ (n : ℕ ), ∃ (m : ℕ), (m ∈ S ∧ m > n)) → S.infinite :=
begin
contrapose!,
intro h,
rw set.not_infinite at h,
let S2 : finset ℕ := set.finite.to_finset h,
have h2 : ∃ B, ∀n ∈ S2, n ≤ B,
{ use finset.sup S2 id,
intros,
apply finset.le_sup H },
cases h2 with N hN,
use N,
intros n hn,
apply hN,
exact (set.finite.mem_to_finset h).symm.mp hn,
end

lemma infinite_iff_arb_large {S : set ℕ } : S.infinite ↔ (∀ (n : ℕ ), ∃ (m : ℕ), (m ∈ S ∧ m > n))
:= iff.intro arb_large_infinite infinite_exists_nat_lt


#### Sam Ezeh (Mar 18 2023 at 22:35):

I'm wondering if this is ok to submit style-wise

lemma infinite_of_forall_exists_nat_lt {S : set ℕ} (h : ∀ (n : ℕ), ∃ m ∈ S, n < m) : S.infinite  :=
begin
intro hS, -- Assume S finite
let S2 : finset ℕ := set.finite.to_finset hS,
have h2 : ∃ B, ∀n ∈ S2, n ≤ B,
{ use finset.sup S2 id,
intros,
apply finset.le_sup H }, -- Exists maximum
cases h2 with N hN, -- N is the maximum
cases h N with n hn, -- n is larger than the maximum
cases hn with hnS hnN, -- n is in S, n is larger than maximum
have h3 := (set.finite.mem_to_finset hS).mpr hnS,
have h4 := hN n,
simp at h4 h3,
have smaller_than_max := h4 h3,
exact nat.le_lt_antisymm smaller_than_max hnN,
end

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, },
{ intro hS,
have exists_nat_lt :=  infinite_of_forall_exists_nat_lt,
finish,
exact S, },
end


#### Eric Wieser (Mar 18 2023 at 22:37):

I recommend you change the statement of infinite_iff_arb_large to match how we rephrased infinite_of_forall_exists_nat_lt; swapping the ∧ for shorter exists notation

#### Eric Wieser (Mar 18 2023 at 22:38):

You should then be able to prove it a single line!

#### Sam Ezeh (Mar 18 2023 at 22:49):

lemma infinite_iff_arb_large  {S : set ℕ } (hs: S.infinite) (hS' : ∀ (n : ℕ), ∃ m ∈ S, n < m)
: S.infinite ↔ ∀ (n : ℕ), ∃ m ∈ S, n < m := iff_of_true hs hS'


Nice!

#### Sam Ezeh (Mar 18 2023 at 22:49):

This was instructive

#### Kevin Buzzard (Mar 18 2023 at 22:51):

PS finish can be super-super-slow. It's great to check something's true but there's almost always a quicker way, and if you get too reliant on it then you end up waiting 10 seconds every time you type a line of code, for the orange bars to disappear.

#### Sam Ezeh (Mar 18 2023 at 22:52):

I'll remember that

#### Sam Ezeh (Mar 18 2023 at 22:54):

I don't need it anymore because of the new one-liner but with the first finish, I had this

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,
sorry, },
{ intro hS,
have exists_nat_lt :=  infinite_of_forall_exists_nat_lt,
finish,
exact S, },
end


This state

S: set ℕ
hS: S.infinite
exists_nat_lt: ∀ (n : ℕ), ∃ (m : ℕ) (H : m ∈ S), n < m
⊢ ∀ (n : ℕ), ∃ (m : ℕ), m ∈ S ∧ n < m


#### Eric Wieser (Mar 18 2023 at 22:54):

That new one liner isn't the right one, your statement says "if A and B then A iff B"

#### Sam Ezeh (Mar 18 2023 at 22:54):

I'll try it once more

#### Eric Wieser (Mar 18 2023 at 22:55):

You need to remove hS and hS' from the statement

#### Sam Ezeh (Mar 18 2023 at 22:58):

That was quite an oversight

lemma infinite_iff_arb_large  {S : set ℕ }
: S.infinite ↔ ∀ (n : ℕ), ∃ m ∈ S, n < m :=
⟨infinite.exists_nat_lt, infinite_of_forall_exists_nat_lt⟩


#### Sam Ezeh (Mar 18 2023 at 22:58):

I learned about the angle bracket notation yesterday

#### Eric Wieser (Mar 18 2023 at 23:02):

That's the one I had in mind!

Last updated: Dec 20 2023 at 11:08 UTC