Zulip Chat Archive

Stream: maths

Topic: compact subset of hausdorff space is closed


view this post on Zulip Edward Ayers (Aug 14 2018 at 18:28):

Hi everyone. I would really appreciate any comments on how to improve this proof. Also, is this result in the library?

import .topological_space
open set filter lattice

universes u v
variables {α : Type u} [ topological_space α]

def inclusion (s : set α) : s -> α := λ a, a
def subspace_top (s : set α) := topological_space.induced (inclusion s)

lemma not_bot_left (f g : filter α) (H1 : f  g  ) : f   := begin
    apply neq_bot_of_le_neq_bot,
    apply H1,
    exact inf_le_left
end

lemma compact_subset_of_t2space_is_closed
    [t2_space α] (Y : set α) (sc : compact Y) : (is_closed Y) := begin
    cases is_closed_iff_nhds, clear mp,
    apply mpr, clear mpr, intros, rename a y,
    let f := (nhds y  principal Y),
    have H3 : ( a (H : a  Y), f  nhds a  ), from sc f a_1 inf_le_right,
    apply exists.elim H3,
    intros, apply exists.elim a_2, intros,
    have H5 : nhds a  nhds y  ,
        rewrite inf_assoc at a_4, -- if I do inf_assoc first it fails?!
        rewrite inf_comm at a_4,
        rewrite inf_assoc at a_4,
        rewrite inf_comm at a_4,
        apply not_bot_left, assumption,
    have H4:  a = y, from eq_of_nhds_neq_bot H5,
    rewrite H4 at a_3,
    assumption
    end

view this post on Zulip Edward Ayers (Aug 14 2018 at 18:54):

Version 2:

lemma compact_subset_of_t2space_is_closed_2
    [t2_space α] (Y : set α) (sc : compact Y) : (is_closed Y) :=
    iff.elim_right is_closed_iff_nhds (λ y H1,
        let f := (nhds y  principal Y) in
        exists.elim (sc f H1 inf_le_right) (λ a H2, exists.elim H2
        (
            assume H3 H4,
            suffices y = a, from by rw this; assumption,
            suffices nhds y  nhds a  principal Y  , from eq_of_nhds_neq_bot $ not_bot_left _ _ this,
            by cc
        )
    )
)

view this post on Zulip Edward Ayers (Aug 14 2018 at 20:14):

Found it in library: closed_of_compact

view this post on Zulip Edward Ayers (Aug 14 2018 at 20:15):

Although I proved it with filters

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:34):

First line of proof could be is_closed_iff_nhds.2 (λ y H1, (iff is a structure and you can access its elements with .1, .2). There's a mathlib style guide and you're not conforming to it (I don't think they like the one-bracket-on-a-line thing, and I know they like 2 spaces indent rather than 4). by rw this; assumption, could be by rwa this (rwa = rw ; assumption, similarly simpa).

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:34):

but it's certainly a darn sight better than I could have done :-)

view this post on Zulip Patrick Massot (Aug 14 2018 at 20:35):

simpa is more than simp ... ; assumption, see https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#simpa

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:45):

Instead of λ a H2, exists.elim H2 ... I wonder if you could have done λ a ⟨H,H2⟩, and then you can maybe avoid the exists.elim

view this post on Zulip Patrick Massot (Aug 14 2018 at 20:45):

Everybody dreams that could be possible, but no.

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:46):

(λ a H3,H4,
        (
            suffices y = a, from by rwa this,

;-)

view this post on Zulip Patrick Massot (Aug 14 2018 at 20:46):

Latest discussion is probably https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/eta.20for.20structures

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:46):

I got lucky because he assumes H3 and H4

view this post on Zulip Edward Ayers (Aug 14 2018 at 20:47):

There's a mathlib style guide

I should read that.

view this post on Zulip Patrick Massot (Aug 14 2018 at 20:50):

Kevin, I don't understand what you wrote? Do you have something that compiles?

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:51):

lemma compact_subset_of_t2space_is_closed_2
  [t2_space α] (Y : set α) (sc : compact Y) : (is_closed Y) :=
is_closed_iff_nhds.2 (λ y H1,
  let f := (nhds y  principal Y) in
  exists.elim (sc f H1 inf_le_right) (λ a ⟨_,_⟩,
    ( suffices y = a, from by rwa this,
      suffices nhds y  nhds a  principal Y  , from eq_of_nhds_neq_bot $ not_bot_left _ _ this,
      by cc)))

My attempt to conform to mathlib style guide but I'm not sure I am -- I don't normally do term mode

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:52):

https://github.com/leanprover/mathlib/blob/master/docs/style.md

view this post on Zulip Patrick Massot (Aug 14 2018 at 20:52):

from by is redundant

view this post on Zulip Patrick Massot (Aug 14 2018 at 20:52):

by is enough

view this post on Zulip Patrick Massot (Aug 14 2018 at 20:52):

how is it possible that λ a ⟨_,_⟩,? Someone lied to me!

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:52):

There's a problem with that idiom

view this post on Zulip Mario Carneiro (Aug 14 2018 at 20:53):

use $ to drop the parentheses and indents

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:53):

It doesn't unfold at all well

view this post on Zulip Mario Carneiro (Aug 14 2018 at 20:53):

it unfolds exactly as well as exists.elim

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:54):

https://github.com/leanprover/mathlib/blob/master/docs/naming.md explains why this lemma is called closed_of_compact

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 20:55):

I should also say that I don't know if any of my suggested changes are _better_, I'm just observing that they exist :-)

view this post on Zulip Mario Carneiro (Aug 14 2018 at 20:57):

there is worth in separating stylistic improvements from proof improvements

view this post on Zulip Mario Carneiro (Aug 14 2018 at 20:58):

space after comma ⟨_, _⟩,

view this post on Zulip Mario Carneiro (Aug 14 2018 at 20:59):

you can use let match in place of exists.elim

view this post on Zulip Edward Ayers (Aug 14 2018 at 21:12):

lemma compact_subset_of_t2space_is_closed_2
  [t2_space α] (Y : set α) (sc : compact Y) : is_closed Y :=
is_closed_iff_nhds.2 $ assume y h₁,
  let a, h₂, h₃ := sc (nhds y  principal Y) h₁ inf_le_right in
  suffices y = a, by rwa this,
  suffices nhds y  nhds a  principal Y  ,
    from eq_of_nhds_neq_bot $ not_bot_left _ _ this,
  by cc

view this post on Zulip Mario Carneiro (Aug 14 2018 at 21:14):

I think you got everything

view this post on Zulip Edward Ayers (Aug 14 2018 at 21:15):

Fabulous thanks so much for your help everyone.

view this post on Zulip Mario Carneiro (Aug 14 2018 at 21:15):

oh, the name needs work

view this post on Zulip Mario Carneiro (Aug 14 2018 at 21:16):

then again closed_of_compact is already taken, I hear

view this post on Zulip Edward Ayers (Aug 14 2018 at 21:19):

Yes I found it in continuity.lean.

view this post on Zulip Edward Ayers (Aug 14 2018 at 21:20):

My big problem with proving this was not knowing what lemmas were available. I would use vscodes find window with regex to find candidate lemmas. Are there any search tools in Lean?

view this post on Zulip Patrick Massot (Aug 14 2018 at 21:20):

tactic.find in mathlib

view this post on Zulip Patrick Massot (Aug 14 2018 at 21:21):

https://github.com/leanprover/mathlib/blob/master/docs/tactics.md

view this post on Zulip Patrick Massot (Aug 14 2018 at 21:21):

Reading mathlib doc would probably be a good idea

view this post on Zulip Patrick Massot (Aug 14 2018 at 21:21):

That find tactic is from Sebastian btw

view this post on Zulip Patrick Massot (Aug 14 2018 at 23:14):

Let me try something more constructive than OS recommendations. Since you like term mode, why isn't the first lemma:
lemma not_bot_left (f g : filter α) (H1 : f ⊓ g ≠ ⊥) : f ≠ ⊥ := neq_bot_of_le_neq_bot H1 inf_le_left

view this post on Zulip Patrick Massot (Aug 14 2018 at 23:19):

and mathlib name would probably be closer to neq_bot_of_inf_neq_bot_left


Last updated: May 18 2021 at 08:14 UTC