complement of finset in infinite set

Stream: new members

[Iocta]

import data.set.basic
import data.set.finite
import data.nat.basic

example (s: set ℕ ) (h: set.finite s) : set.infinite sᶜ := _

Is this in mathlib?

[Iocta]

I started working on it but it seemed to need a bunch of lemmas I couldn't find

[Adam Topaz]

I wonder if there is a straightforward proof with cardinality?

[Alex J. Best]

mk_compl_of_omega_le seems useful?

[Adam Topaz]

Presumably there is also a lemma stating that a set of cardinality omega is infinite?

[Alex J. Best]

open cardinal
example (s: set ℕ ) (h: set.finite s) : set.infinite sᶜ :=
begin
  rw [← set.infinite_coe_iff, infinite_iff, mk_compl_of_omega_le s _ _],
  all_goals {rw mk_nat,},
  exact lt_omega_iff_finite.mpr h,
end

[Alex J. Best]

Probably this can be made into a 2-liner xD

[Kyle Miller]

I don't know how to navigate the finset/fintype API well enough to finish this quickly, but another approach is to first transform it by something like

example (s: set ℕ) (h: set.finite s) : set.infinite sᶜ :=
begin
  intro h',
  tactic.unfreeze_local_instances,
  cases h, cases h',
  dsimp [compl, boolean_algebra.compl, set.compl] at h',
  sorry
end

so then the context is

s : set ℕ,
h : fintype ↥s,
h' : fintype ↥{a : ℕ | a ∉ s}
⊢ false

If you let m and m' be the maximal elements in the two sets, then 1 + max m m' is in neither set, contradicting the fact that the sets are complements.

[Kyle Miller]

(I know the question is "is this in mathlib," which this certainly doesn't help you in answering.)

[Mario Carneiro]

I would suggest:

example (s: set ℕ) (h: set.finite s) : set.infinite sᶜ :=
begin
  intro h',
  apply set.infinite_univ_iff.2 nat.infinite,
  simpa using h.union h',
end

[Kenny Lau]

example (s : set ℕ) (hs : set.finite s) : set.infinite sᶜ :=
λ hsc, @set.infinite_univ ℕ _ $ set.union_compl_self s ▸ hs.union hsc