infinite_iff_arb_large

Stream: new members

[Sam Ezeh]

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]

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

[Sam Ezeh]

Thank you!

[Eric Wieser]

I've granted you (dignissimus) write access!

[Yaël Dillies]

Incidentally, #18604 is relevant.

[Sam Ezeh]

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]

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

[Sam Ezeh]

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]

Did you run leanproject get-cache?

[Eric Wieser]

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

[Sam Ezeh]

leanproject get-cachee was what I needed

[Sam Ezeh]

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

[Sam Ezeh]

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]

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]

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]

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

[Sam Ezeh]

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]

This was instructive

[Kevin Buzzard]

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]

I'll remember that

[Sam Ezeh]

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]

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

[Sam Ezeh]

I'll try it once more

[Eric Wieser]

You need to remove hS and hS' from the statement

[Sam Ezeh]

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]

I learned about the angle bracket notation yesterday

[Eric Wieser]

That's the one I had in mind!