Finite set induction and complement

Stream: new members

[Pedro Minicz]

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]

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]

I would suggest avoiding induction

[Mario Carneiro]

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

[Pedro Minicz]

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]

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]

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]

and I already found a use for rintro x -,

[Pedro Minicz]

Great, thank you! I usually forget about convert, good to be reminded about it!