Zulip Chat Archive

Stream: new members

Topic: Finite set induction and complement


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 22:12):

I would suggest avoiding induction

view this post on Zulip Mario Carneiro (Aug 19 2020 at 22:12):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 22:23):

and I already found a use for rintro x -,

view this post on Zulip 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