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