# Zulip Chat Archive

## 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