# Zulip Chat Archive

## Stream: new members

### Topic: Finite set induction and complement

#### Pedro Minicz (Aug 19 2020 at 21:28):

I feel like I am missing something in the following proof. `set.finite.induction_on`

doesn't work on the goal, but I feel like there should be some `set.finite.dinduction`

cleverness that I am missing.

```
import topology.order
variables {α : Type*} {s : set α}
example (hs : sᶜ.finite) :
topological_space.generate_open {s | ∃! x, x ∉ s} s :=
sorry
```

#### Pedro Minicz (Aug 19 2020 at 21:53):

A work-in-progress. Not sure if this strategy is going to work.

```
import topology.order
variables {α : Type*} {s : set α}
@[simp] def p : set α → Prop :=
λ s, topological_space.generate_open {s | ∃! x, x ∉ s} sᶜ
example (hs : sᶜ.finite) :
topological_space.generate_open {s | ∃! x, x ∉ s} s :=
begin
suffices : p sᶜ, by simpa,
apply set.finite.induction_on hs,
{ simp [p, topological_space.generate_open.univ] },
{ intros x s hx hs H,
simp only [p] at *,
sorry }
end
```

#### Mario Carneiro (Aug 19 2020 at 22:12):

I would suggest avoiding induction

#### Mario Carneiro (Aug 19 2020 at 22:12):

there should be a way to directly apply topology theorems to get this

#### Pedro Minicz (Aug 19 2020 at 22:20):

Managed to prove it using said strategy.

```
import topology.order
variables {α : Type*} {s : set α}
@[simp] def p : set α → Prop :=
λ s, topological_space.generate_open {s | ∃! x, x ∉ s} sᶜ
example (hs : sᶜ.finite) :
topological_space.generate_open {s | ∃! x, x ∉ s} s :=
begin
suffices : p sᶜ, by simpa,
apply set.finite.induction_on hs,
{ simp [p, topological_space.generate_open.univ] },
{ intros x s hx hs ih,
simp only [p] at *,
suffices : (insert x s)ᶜ = sᶜ ∩ {x}ᶜ,
{ rw this,
apply topological_space.generate_open.inter _ _ ih,
apply topological_space.generate_open.basic,
use x,
simp },
ext y,
conv
{ congr,
simp [not_or_distrib],
skip,
simp [not_or_distrib] },
rw and_comm }
end
```

#### Pedro Minicz (Aug 19 2020 at 22:21):

Mario Carneiro said:

there should be a way to directly apply topology theorems to get this

I'll give it a look. I am not very familiar with topology, I'll try to keep it in mind while I study it.

#### Mario Carneiro (Aug 19 2020 at 22:22):

```
example (hs : sᶜ.finite) :
topological_space.generate_open {s | ∃! x, x ∉ s} s :=
begin
convert @is_open_bInter _ _ (topological_space.generate_from {s | ∃! x, x ∉ s}) _
(λ a, ({a} : set α)ᶜ) hs _,
{ ext x, simp [not_imp_not] },
{ intros x _,
apply topological_space.generate_open.basic,
use x, simp }
end
```

#### Mario Carneiro (Aug 19 2020 at 22:23):

and I already found a use for `rintro x -,`

#### Pedro Minicz (Aug 19 2020 at 22:35):

Great, thank you! I usually forget about `convert`

, good to be reminded about it!

Last updated: May 09 2021 at 18:17 UTC