# Zulip Chat Archive

## Stream: maths

### Topic: compact subset of hausdorff space is closed

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

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

#### Edward Ayers (Aug 14 2018 at 20:14):

Found it in library: `closed_of_compact`

#### Edward Ayers (Aug 14 2018 at 20:15):

Although I proved it with filters

#### 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`

).

#### Kevin Buzzard (Aug 14 2018 at 20:34):

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

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

#### 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`

#### Patrick Massot (Aug 14 2018 at 20:45):

Everybody dreams that could be possible, but no.

#### Kevin Buzzard (Aug 14 2018 at 20:46):

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

;-)

#### Patrick Massot (Aug 14 2018 at 20:46):

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

#### Kevin Buzzard (Aug 14 2018 at 20:46):

I got lucky because he assumes `H3`

and `H4`

#### Edward Ayers (Aug 14 2018 at 20:47):

There's a mathlib style guide

I should read that.

#### Patrick Massot (Aug 14 2018 at 20:50):

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

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

#### Kevin Buzzard (Aug 14 2018 at 20:52):

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

#### Patrick Massot (Aug 14 2018 at 20:52):

`from by`

is redundant

#### Patrick Massot (Aug 14 2018 at 20:52):

`by`

is enough

#### Patrick Massot (Aug 14 2018 at 20:52):

how is it possible that `λ a ⟨_,_⟩,`

? Someone lied to me!

#### Kevin Buzzard (Aug 14 2018 at 20:52):

There's a problem with that idiom

#### Mario Carneiro (Aug 14 2018 at 20:53):

use `$`

to drop the parentheses and indents

#### Kevin Buzzard (Aug 14 2018 at 20:53):

It doesn't unfold *at all* well

#### Mario Carneiro (Aug 14 2018 at 20:53):

it unfolds exactly as well as `exists.elim`

#### 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`

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

#### Mario Carneiro (Aug 14 2018 at 20:57):

there is worth in separating stylistic improvements from proof improvements

#### Mario Carneiro (Aug 14 2018 at 20:58):

space after comma ` ⟨_, _⟩,`

#### Mario Carneiro (Aug 14 2018 at 20:59):

you can use `let`

match in place of `exists.elim`

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

#### Mario Carneiro (Aug 14 2018 at 21:14):

I think you got everything

#### Edward Ayers (Aug 14 2018 at 21:15):

Fabulous thanks so much for your help everyone.

#### Mario Carneiro (Aug 14 2018 at 21:15):

oh, the name needs work

#### Mario Carneiro (Aug 14 2018 at 21:16):

then again `closed_of_compact`

is already taken, I hear

#### Edward Ayers (Aug 14 2018 at 21:19):

Yes I found it in `continuity.lean`

.

#### 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?

#### Patrick Massot (Aug 14 2018 at 21:20):

tactic.find in mathlib

#### Patrick Massot (Aug 14 2018 at 21:21):

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

#### Patrick Massot (Aug 14 2018 at 21:21):

Reading mathlib doc would probably be a good idea

#### Patrick Massot (Aug 14 2018 at 21:21):

That find tactic is from Sebastian btw

#### 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`

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