## Stream: new members

### Topic: complement of finset in infinite set

#### Iocta (Aug 19 2020 at 00:19):

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 (Aug 19 2020 at 00:22):

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

#### Adam Topaz (Aug 19 2020 at 00:33):

I wonder if there is a straightforward proof with cardinality?

#### Alex J. Best (Aug 19 2020 at 00:34):

mk_compl_of_omega_le seems useful?

#### Adam Topaz (Aug 19 2020 at 00:35):

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

#### Alex J. Best (Aug 19 2020 at 00:44):

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 (Aug 19 2020 at 00:45):

Probably this can be made into a 2-liner xD

#### Kyle Miller (Aug 19 2020 at 00:50):

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 (Aug 19 2020 at 00:51):

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

#### Mario Carneiro (Aug 19 2020 at 01:00):

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 (Aug 19 2020 at 06:40):

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


Last updated: May 15 2021 at 00:39 UTC