compact subset of hausdorff space is closed

Stream: maths

[Edward Ayers]

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

[Edward Ayers]

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
        )
    )
)

[Edward Ayers]

Found it in library: closed_of_compact

[Edward Ayers]

Although I proved it with filters

[Kevin Buzzard]

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).

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

Everybody dreams that could be possible, but no.

[Kevin Buzzard]

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

;-)

[Patrick Massot]

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

[Kevin Buzzard]

I got lucky because he assumes H3 and H4

[Edward Ayers]

There's a mathlib style guide

I should read that.

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

from by is redundant

[Patrick Massot]

by is enough

[Patrick Massot]

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

[Kevin Buzzard]

There's a problem with that idiom

[Mario Carneiro]

use $ to drop the parentheses and indents

[Kevin Buzzard]

It doesn't unfold at all well

[Mario Carneiro]

it unfolds exactly as well as exists.elim

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

there is worth in separating stylistic improvements from proof improvements

[Mario Carneiro]

space after comma ⟨_, _⟩,

[Mario Carneiro]

you can use let match in place of exists.elim

[Edward Ayers]

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

[Mario Carneiro]

I think you got everything

[Edward Ayers]

Fabulous thanks so much for your help everyone.

[Mario Carneiro]

oh, the name needs work

[Mario Carneiro]

then again closed_of_compact is already taken, I hear

[Edward Ayers]

Yes I found it in continuity.lean.

[Edward Ayers]

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?

[Patrick Massot]

tactic.find in mathlib

[Patrick Massot]

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

[Patrick Massot]

Reading mathlib doc would probably be a good idea

[Patrick Massot]

That find tactic is from Sebastian btw

[Patrick Massot]

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

[Patrick Massot]

and mathlib name would probably be closer to neq_bot_of_inf_neq_bot_left