# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: disjoint_nhds_finite_of_t2

#### Damiano Testa (Dec 11 2020 at 08:33):

Dear All,

is there a lemma extending the "T_2 property" of a topological space from two points to a `finset`

? I am thinking of something along the lines of the lemma below, but any essentially equivalent formulation would likely work!

Thanks!

```
import topology.separation
import data.finsupp
--instance (X : Type*) : has_zero (set X) := ⟨(∅ : set X)⟩
-- Lean complains:
-- invalid definition, a declaration named 'set.has_zero' has already been declared
lemma disjoint_nhds_finset_of_t2 {X : Type*} [topological_space X] [t2_space X] (s : finset X) :
∃ U : @finsupp X (set X) ⟨∅⟩, -- awkward: I think that this instance should be there...
(∀ a : X, a ∈ s → (U a) ∈ nhds a) ∧
∀ a b : X, a ∈ s → b ∈ s → disjoint (U a) (U b) :=
begin
sorry
/- -- proof likely starting with
generalize' hd : s.card = d,
refine finset.induction_on s _ _,
-/
end
```

#### Damiano Testa (Dec 11 2020 at 09:10):

Related to the above: is it possible define a function `f : X → X → set X × set X`

with the property that, if `x ≠ y`

, then `f x y = (U, V)`

with `U`

and `V`

disjoint neighbourhoods of `x`

and `y`

? In the sample below, `cases`

complains:

```
induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop
```

I take this to mean that `cases`

can only return stuff of Type `Prop`

, but in this case would have to return something of Type `set X`

?

```
def disjoint_opens_pairs_of_t2 {X : Type*} [topological_space X] [t2_space X] :
X → X → set X × set X :=
begin
intros x y,
by_cases xy : x = y,
{ exact ⟨set.univ, set.univ⟩ },
cases t2_space.t2 x y xy,
end
```

#### Damiano Testa (Dec 11 2020 at 09:13):

(I realize that, depending on how `t2_space`

is implemented, this might require the axiom of choice: I am happy to assume it!)

#### Mario Carneiro (Dec 11 2020 at 09:19):

yes, it is possible. Start by proving `\forall x y, \exists (UV : set X × set X), <disjoint yada yada>`

#### Mario Carneiro (Dec 11 2020 at 09:19):

and then use `classical.some`

on this proof to get the function

#### Damiano Testa (Dec 11 2020 at 09:20):

Thanks for the suggestion: I will try!

#### Mario Carneiro (Dec 11 2020 at 09:22):

oh, actually I see there is a case disjunction, so I guess you want the proof to be `\forall x y, x != y -> \exists (UV : set X × set X), <disjoint yada yada>`

, and then the function is `\lam x y, if h : x = y then (univ, univ) else classical.some (proof x y h)`

#### Damiano Testa (Dec 11 2020 at 09:29):

The definition of `t2_space`

seems to be exactly what I should prove, right?

```
class t2_space (α : Type u) [topological_space α] : Prop :=
(t2 : ∀x y, x ≠ y → ∃u v : set α, is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ u ∩ v = ∅)
```

#### Damiano Testa (Dec 11 2020 at 09:46):

Thank you, Mario! The code below compiles and I think that it does what I want!

```
lemma pre_choice_opens (X : Type*) [topological_space X] [t2_space X] :
∀ x y : X, x ≠ y → ∃ (U : set X × set X),
is_open U.1 ∧ is_open U.2 ∧ x ∈ U.1 ∧ y ∈ U.2 ∧ U.1 ∩ U.2 = ∅ :=
begin
intros x y xy,
rcases (t2_separation xy) with ⟨U, V, Z⟩,
refine ⟨(U, V), Z⟩,
end
def t2_choice (X : Type*) [topological_space X] [t2_space X] :
X → X → set X × set X :=
λ x y, if h : x = y then (set.univ, set.univ) else classical.some (pre_choice_opens X x y h)
#check t2_choice
-- t2_choice : Π (X : Type u_2) [_inst_4 : topological_space X] [_inst_5 : t2_space X], X → X → set X × set X
```

#### Mario Carneiro (Dec 11 2020 at 09:48):

I suggest actually making two definitions, for the two sets, and then three lemmas about the properties of the two sets (all unpacked from the `pre_choice_opens`

proof)

#### Damiano Testa (Dec 11 2020 at 09:49):

I think that I am misunderstanding: the two sets need to be disjoint: how can I define them separately?

#### Patrick Massot (Dec 11 2020 at 10:56):

Mario, this kind of trick is really difficult for beginners (or even intermediate users like Damiano).

#### Patrick Massot (Dec 11 2020 at 10:57):

Damanio, here are the definitions and statements. You need to understand docs#classical.some and docs#classical.some_spec.

```
import topology.separation
noncomputable theory
open topological_space set classical
open_locale classical
variables {X : Type*} [topological_space X] [t2_space X]
def t2_open₁ (x y : X) : set X :=
if h : x = y then univ else (some (t2_separation h))
def t2_open₂ (x y : X) : set X :=
if h : x = y then univ else (some $ some_spec $ t2_separation h)
lemma mem_t2_open₁ (x y : X) : x ∈ t2_open₁ x y :=
sorry
lemma mem_t2_open₂ (x y : X) : y ∈ t2_open₂ x y :=
sorry
lemma disjoint_t2_open₁_t2_open₂ {x y : X} (h : x ≠ y) : t2_open₁ x y ∩ t2_open₂ x y = ∅ :=
sorry
```

#### Patrick Massot (Dec 11 2020 at 10:58):

And it misses two lemmas saying both sets are open.

#### Patrick Massot (Dec 11 2020 at 10:58):

I can give you the proofs if you get stuck, but this is an important exercise.

#### Patrick Massot (Dec 11 2020 at 11:00):

The missing statements are

```
lemma is_open_t2_open₁ (x y : X) : is_open (t2_open₁ x y) :=
sorry
lemma is_open_t2_open₂ (x y : X) : is_open (t2_open₂ x y) :=
sorry
```

#### Damiano Testa (Dec 11 2020 at 11:01):

Let me give it a try! Thanks!

#### Patrick Massot (Dec 11 2020 at 11:01):

Note that all proofs are two to four lines long.

#### Patrick Massot (Dec 11 2020 at 11:02):

Note also where is the "precondition" `x ≠ y`

. You don't need it to talk about the open sets, and you don't need it in 4 lemmas out of 5.

#### Patrick Massot (Dec 11 2020 at 11:02):

That's the key: you don't want to pass around proofs to talk about objects only when proving the crucial property.

#### Damiano Testa (Dec 11 2020 at 11:03):

Ok, this concept is slowly creeping its way in me, although it is not easy for me to spot where I am making this error...

#### Patrick Massot (Dec 11 2020 at 11:05):

I know it feels weird but only because you're usually lying to yourself. When you write computations on paper, it's not true that for each division you write a proof next to the division symbol. So you're doing the same thing as we do here: write first, apologize later.

#### Patrick Massot (Dec 11 2020 at 11:09):

Note also the trick that junk values (this is how we call values returned when the precondition is not met) are not random, although Kevin loves to joke about returning 37. They are carefully chosen to maximize the number of lemmas that are unconditionnaly true. For instance here, returning the empty set would be a bad choice because `mem_t2_open₁`

would need the precondition. Again we don't really care those lemmas are true in junk cases, but it does save some typing when applying them.

#### Damiano Testa (Dec 11 2020 at 11:32):

This is my attempt with the first of the lemmas above: I am not even sure if I made progress or not...

```
lemma mem_t2_open₁ (x y : X) : x ∈ t2_open₁ x y :=
begin
unfold t2_open₁,
split_ifs,
exact mem_univ x,
obtain F := (t2_separation h),
-- obtain ⟨U, V, oU, oV, xU, yV, UV⟩ := (t2_separation h),
rw mem_def,
```

For me, the `some`

is a wall that I cannot climb...

#### Damiano Testa (Dec 11 2020 at 11:33):

I did identify the `_`

in the underscore as `F`

, though! This is the only use that I have for the `obtain`

line...

#### Mario Carneiro (Dec 11 2020 at 11:33):

Whenever you see a `some`

, use `some_spec`

with the same hypothesis given to `some`

#### Damiano Testa (Dec 11 2020 at 11:33):

Ah, I will try! Thanks!

#### Damiano Testa (Dec 11 2020 at 12:00):

This is a proof of the first lemma!

```
lemma mem_t2_open₁ (x y : X) : x ∈ t2_open₁ x y :=
begin
unfold t2_open₁,
split_ifs,
exact mem_univ x,
rcases (some_spec (t2_separation h)) with ⟨_, _, _, D, _⟩,
exact D,
end
```

Any comments are very welcome! Especially since I do not really understand this proof (or rather, what it is that I am supposed to prove)!

#### Mario Carneiro (Dec 11 2020 at 12:01):

That's right. You can probably write it as something like `(some_spec (t2_separation h)).snd.2.2.1`

#### Mario Carneiro (Dec 11 2020 at 12:02):

Basically, `some_spec (t2_separation h)`

is a theorem that says `some (t2_separation h)`

satisfies the property in the existential of `t2_separation h`

#### Mario Carneiro (Dec 11 2020 at 12:04):

in this case, `some (t2_separation h)`

is `t2_open₁ x y`

, so `some_spec (t2_separation h)`

says that `∃v : set α, is_open (t2_open₁ x y) ∧ is_open v ∧ x ∈ t2_open₁ x y ∧ y ∈ v ∧ t2_open₁ x y ∩ v = ∅)`

#### Damiano Testa (Dec 11 2020 at 12:06):

Ok, so it is giving a name to the "variable" open set that contains x and [properties involving y], without referring to y. Is this a correct way of thinking about this?

#### Mario Carneiro (Dec 11 2020 at 12:07):

I find it a bit easier to understand if there is only one existential; Patrick's version uses `some`

twice on the two existentials. If you use `some`

on your `pre_choice_opens`

proof instead of `t2_separation h`

directly, the property you get out is something like `is_open (foo x y).1 ∧ is_open (foo x y).2 ∧ x ∈ (foo x y).1 ∧ y ∈ (foo x y).2 ∧ (foo x y).1 ∩ (foo x y).2 = ∅)`

, where `foo x y`

is a definition abbreviating `some (pre_choice_opens x y h)`

. If you then define `t2_open₁ x y := (foo x y).1`

and `t2_open₂ x y := (foo x y).2`

, then you can simply observe that this is a conjunction of all the lemmas you want

#### Damiano Testa (Dec 11 2020 at 12:11):

I think that the "nested" `some`

s are now what I am trying to undo in the second lemma. I will try to fill in the proofs with both approaches: I may learn `some`

thing

#### Damiano Testa (Dec 11 2020 at 12:43):

It took me a while, but here is a proof of lemma 2:

```
lemma mem_t2_open₂ (x y : X) : y ∈ t2_open₂ x y :=
begin
unfold t2_open₂,
split_ifs,
exact mem_univ _,
rcases some_spec (some_spec (t2_separation h)) with ⟨_, _, _, D, _⟩,
exact D,
end
```

#### Patrick Massot (Dec 11 2020 at 13:01):

The fact there are two existentials is indeed a bit unfortunate for a first exercise in using these ideas. The reason I did that is the existing lemma `t2_separation`

is stated like that.

#### Patrick Massot (Dec 11 2020 at 13:02):

My proofs were:

```
lemma mem_t2_open₁ (x y : X) : x ∈ t2_open₁ x y :=
begin
by_cases h : x = y,
{ simp [t2_open₁, h] },
{ rcases some_spec (t2_separation h) with ⟨op₁, op₂, x_in, y_in, hinter⟩,
simpa [t2_open₁, h] using T }
end
lemma mem_t2_open₂ (x y : X) : y ∈ t2_open₂ x y :=
begin
by_cases h : x = y,
{ simp [t2_open₂, h] },
{ rcases some_spec (some_spec $ t2_separation h) with ⟨-, -, -, y_in, -⟩,
simpa [t2_open₂, h] using y_in }
end
```

In the first proof I named every pieces in the `rcases`

for clarity, and in the second lemma I illustrate how to throw away unneeded pieces.

#### Damiano Testa (Dec 11 2020 at 13:05):

Thanks for your proofs! I also had all the terms in the `rcases ... ⟨_, _, _, D, _⟩`

labeled, but then I dropped them, for obscurity!

#### Patrick Massot (Dec 11 2020 at 13:06):

Underscores do not drop them, it gives them awful names. Dashes drop them.

#### Damiano Testa (Dec 11 2020 at 13:06):

here is a proof of the next lemma:

```
lemma disjoint_t2_open₁_t2_open₂ {x y : X} (h : x ≠ y) : t2_open₁ x y ∩ t2_open₂ x y = ∅ :=
begin
unfold t2_open₂,
split_ifs,
{ exfalso,
exact h h_1 },
{ unfold t2_open₁,
split_ifs,
rcases some_spec (some_spec (t2_separation h)) with ⟨_, _, _, _, E⟩,
exact E },
end
```

#### Damiano Testa (Dec 11 2020 at 13:07):

Patrick Massot said:

Underscores do not drop them, it gives them awful names. Dashes drop them.

Ah, I learned that

- I should pay more attention to the difference between
`-`

and`_`

; - there
*is*a difference between them!

#### Patrick Massot (Dec 11 2020 at 13:08):

Ok, now try to prove that next lemma in two lines (one `rcases`

and one more line).

#### Damiano Testa (Dec 11 2020 at 13:08):

Seeing your proofs, I could probably avoid `unfold`

ing and separate the cases presciently...

#### Patrick Massot (Dec 11 2020 at 13:08):

I mean `disjoint_t2_open₁_t2_open₂`

#### Damiano Testa (Dec 11 2020 at 13:09):

Yes, it is the next one in your/my list!

Except it is almost lunch time: I might do it in a bit!

Thanks for the exercises and the help!

#### Patrick Massot (Dec 11 2020 at 13:10):

No, it's what you called the next one, but you just pasted a proof that is 8 lines long.

#### Patrick Massot (Dec 11 2020 at 13:10):

I say make it 2 lines long now.

#### Damiano Testa (Dec 11 2020 at 13:10):

Ah, ok!

#### Damiano Testa (Dec 11 2020 at 13:11):

(sorry, I was still processing the `_`

and `-`

)

#### Patrick Massot (Dec 11 2020 at 13:12):

Actually you can make it one line long (without cheating by putting two tactics on the same line) if you go to 106 columns.

#### Patrick Massot (Dec 11 2020 at 13:13):

Oh, I can bring it down to 89 columns, but this is borderline obfuscation.

#### Patrick Massot (Dec 11 2020 at 13:14):

I should really work now instead of playing with Lean.

#### Patrick Massot (Dec 11 2020 at 13:20):

Admittedly, all this is trivial after seeing the definition of T2, so obfuscation is allowed:

```
lemma is_open_t2_open₂ (x y : X) : is_open (t2_open₂ x y) :=
(classical.em $ x = y).elim (λ h, by simp [t2_open₂, h])
(λ h, by simpa [t2_open₂, h] using (some_spec $ some_spec $ t2_separation h).2.1)
```

Ok, I'll go to work.

#### Damiano Testa (Dec 11 2020 at 13:29):

I'll need time to process these two lines: for the moment, I will absorb the satisfaction that I could find *one* proof!

#### Damiano Testa (Dec 11 2020 at 17:21):

I feel at the same time proud and ashamed: I managed to prove the statement about disjoint `finset`

s having disjoint neighbourhoods... but not using `some`

s... sorry! Below is the argument, in case people are interested!

```
import topology.separation
noncomputable theory
open topological_space set finset
open_locale classical
lemma finset_disjoint_point_opens_of_t2
{X : Type*} [topological_space X] [t2_space X] (s : finset X) :
∀ (x : X), x ∉ s →
∃ U V : (set X), (is_open U) ∧ is_open V ∧ (∀ a : X, a ∈ s → a ∈ U) ∧ x ∈ V ∧ disjoint U V :=
begin
generalize' hd : s.card = d,
refine finset.induction_on s _ _,
{ refine λ _ _, ⟨∅, set.univ, is_open_empty, is_open_univ, λ x h, by cases h, set.mem_univ _, _⟩,
exact set.disjoint_univ.mpr rfl },
rintros a t ta xxt x xt,
obtain ⟨U, V, oU, oV, xU, aV, UV⟩ := @t2_separation _ _ _ x a _,
have : x ∉ t := λ j, xt (mem_insert_of_mem j),
obtain ⟨Ui, Vi, oUi, oVi, xUi, aVi, UVi⟩ := xxt x this,
refine ⟨V ∪ Ui, U ∩ Vi, is_open_union oV oUi, is_open_inter oU oVi, _, ⟨xU, aVi⟩, _⟩,
{ intros f fi,
by_cases fa : f = a,
{ subst fa, exact set.mem_union_left _ aV },
apply set.mem_union_right,
apply xUi f,
apply mem_of_mem_insert_of_ne fi fa },
{ apply disjoint.union_left _ (set.disjoint_of_subset_right (set.inter_subset_right U Vi) UVi),
{ apply @set.disjoint_of_subset_right _ V (U ∩ Vi) U (set.inter_subset_left U Vi),
rw set.inter_comm at UV,
exact set.disjoint_iff_inter_eq_empty.mpr UV } },
symmetry,
exact ne_of_mem_of_not_mem (mem_insert_self a t) xt,
end
lemma finset_disjoint_finset_opens_of_t2
{X : Type*} [topological_space X] [t2_space X] (s t : finset X) :
disjoint s t →
∃ U V : (set X), (is_open U) ∧ is_open V ∧ (∀ a : X, a ∈ s → a ∈ U) ∧ (∀ a : X, a ∈ t → a ∈ V)
∧ disjoint U V :=
begin
generalize' hd : t.card = d,
refine finset.induction_on t _ _,
{ intros f,
refine ⟨set.univ, ∅, is_open_univ, is_open_empty, λ _ _, set.mem_univ _, λ a h, by cases h, _⟩,
exact set.univ_disjoint.mpr rfl },
{ intros x S xS hi sxS,
obtain ⟨U, V, oU, oV, xU, yV, UV⟩ := hi (finset.disjoint_of_subset_right (subset_insert x S) sxS),
obtain ⟨Ui, Vi, oUi, oVi, xUi, aVi, UiVi⟩ := finset_disjoint_point_opens_of_t2 s x _,
{ refine ⟨U ∩ Ui, V ∪ Vi, is_open_inter oU oUi, is_open_union oV oVi, _, _, _⟩,
{ refine λ a as, ⟨xU a as, xUi a as⟩ },
{ intros f fi,
by_cases fx : f = x,
{ subst fx, apply set.mem_union_right _ aVi },
{ exact Vi.mem_union_left (yV f (mem_of_mem_insert_of_ne fi fx)) } },
{ apply disjoint.union_right,
{ exact set.disjoint_of_subset_left (set.inter_subset_left U Ui) UV },
{ exact set.disjoint_of_subset_left (set.inter_subset_right U Ui) UiVi } } },
{ exact (disjoint_insert_right.mp sxS).1 } },
end
```

#### Eric Wieser (Dec 11 2020 at 19:32):

.

#### Damiano Testa (Dec 12 2020 at 05:45):

In case this is not already in mathlib and people think that this is a useful addition, I can make a PR with this proof!

:smile:

#### Adam Topaz (Dec 12 2020 at 05:51):

I guess there's al ultrafilter-centric analogue of this statement too... (analogous to docs#t2_iff_ultrafilter )

#### Damiano Testa (Dec 12 2020 at 05:53):

I did not learn about ultrafilters yet: I will make this PR and see if there is interest in more!

#### Adam Topaz (Dec 12 2020 at 05:54):

But maybe it's not that interesting... I guess it would say, approximately, that given any two disjoint finite sets `S`

and `T`

, any ultrafilter which converges to a point in `S`

cannot converge to any point in `T`

.

#### Adam Topaz (Dec 12 2020 at 05:56):

@Damiano Testa I didn't like ultrafilters at first, but then I realized that one should think of them like algebraic geometers think of valuation rings, and now I love them!

#### Damiano Testa (Dec 12 2020 at 05:57):

Ah, as I am not familiar with filters/ultrafilters, I unconsciously try to avoid them. Your comment makes me want to dive into them, though! Thanks!

#### Adam Topaz (Dec 12 2020 at 06:03):

(The analogy breaks down after a while, but it's a good approximation :smile: )

#### Damiano Testa (Dec 12 2020 at 06:33):

Done!

#5332

Let's see if Lean also likes it!

#### Damiano Testa (Dec 12 2020 at 18:50):

The code below proves the same existence of disjoint open sets containing disjoint finsets. It is slightly longer than the other proof, however it seems more streamlined: should I update the previous PR or, by proof-irrelevance, the shorter the proof, the better?

Here, short is only measured in terms of lines, not of anything more objective.

```
import topology.separation
import data.fintype.basic
open_locale classical
open set
lemma finset_ind_card_empty {X : Type*} (P : finset X → finset X → Prop)
(symm : ∀ {a b}, P a b → P b a)
(basea0 : ∀ {a}, P a ∅)
(base11 : ∀ {a b}, P {a} {b})
(indu : ∀ {a b c}, P a c → P b c → P (a ∪ b) c) :
∀ a b, P a b :=
begin
intros a b,
refine finset.induction_on b basea0 (λ x s xs hi, symm _),
rw finset.insert_eq,
apply indu _ (symm hi),
refine finset.induction_on a basea0 (λ a t ta hi, symm _),
rw finset.insert_eq,
exact indu base11 (symm hi),
end
def dis {α : Type*} [topological_space α] : finset α → finset α → Prop :=
λ (s t : finset α), disjoint s t → ∃ U V : (set α), (is_open U) ∧ is_open V ∧
(∀ a : α, a ∈ s → a ∈ U) ∧ (∀ a : α, a ∈ t → a ∈ V) ∧ disjoint U V
lemma dis_symm {α : Type*} [topological_space α] (s t : finset α) : dis s t → dis t s :=
begin
intros h1 d,
unfold dis at h1,
obtain ⟨U, V, oU, oV, aU, bV, UV⟩ := h1 (disjoint.symm d),
exact ⟨V, U, oV, oU, bV, aU, disjoint.symm UV⟩
end
lemma dis_basea0 {α : Type*} [topological_space α] : ∀ {a : finset α}, dis a ∅ :=
λ a d, ⟨_, _, is_open_univ, is_open_empty, λ a h, mem_univ a, λ a h, by cases h, disjoint_empty _⟩
lemma dis_base11 {α : Type*} [topological_space α] [t2_space α] : ∀ {a b : α}, dis ({a} : finset α) {b} :=
begin
intros a b d,
simp only [forall_eq, finset.mem_singleton, disjoint_iff_inter_eq_empty],
exact t2_separation (finset.not_mem_singleton.mp (finset.disjoint_singleton.mp (disjoint.comm.mp d))),
end
lemma dis_indu {α : Type*} [topological_space α] : ∀ {a b c : finset α}, dis a c → dis b c → dis (a ∪ b) c :=
begin
intros a b c ac bc d,
obtain ⟨U1, V1, oU1, oV1, aU1, bV1, UV1⟩ := ac (finset.disjoint_of_subset_left (finset.subset_union_left _ _) d),
obtain ⟨U2, V2, oU2, oV2, aU2, bV2, UV2⟩ := bc (finset.disjoint_of_subset_left (finset.subset_union_right _ _) d),
refine ⟨U1 ∪ U2, V1 ∩ V2, is_open_union oU1 oU2, is_open_inter oV1 oV2, λ x xab, _, λ x xc, ⟨bV1 _ xc, bV2 _ xc⟩, _⟩,
{ cases finset.mem_union.mp xab with h h,
{ exact mem_union_left U2 (aU1 x h) },
{ exact mem_union_right U1 (aU2 x h) } },
{ apply disjoint_union_left.mpr,
refine ⟨disjoint_of_subset_right (inter_subset_left _ _) UV1, disjoint_of_subset_right (inter_subset_right _ _) UV2⟩ },
end
lemma disjoint_finset_t2 {α : Type*} [topological_space α] [t2_space α] : ∀ (s t : finset α), dis s t :=
finset_ind_card_empty dis dis_symm (λ _, dis_basea0) (λ _ _, dis_base11) (λ _ _ _, dis_indu)
```

#### Damiano Testa (Dec 12 2020 at 18:56):

~~Also, why in the last proof, I need to use the underscores? I would have wanted to use ~~`dis_basea0`

and the others, just like I did `dis_symm`

, but I cannot understand why Lean does not like it.

#### Bhavik Mehta (Dec 12 2020 at 18:56):

Probably `dis_basea0`

takes some extra arguments which `apply`

automatically figures out - similarly if you change the `apply dis_basea0`

to `refine disbasea0`

, it'll probably fail

#### Bhavik Mehta (Dec 12 2020 at 18:57):

You can use `show_term {apply dis_basea0}`

to see what you could use in place of that refine, and then put that instead of the underscore

#### Damiano Testa (Dec 12 2020 at 18:58):

Thanks! I fixed the first two: I am still not entirely sure what it is, but the new version works!

#### Damiano Testa (Dec 12 2020 at 19:07):

I had tried `show_term`

but it gives something that does not work. If I remember correctly, it said `exact dis_basea0`

.

#### Damiano Testa (Dec 13 2020 at 05:09):

I pushed a more conceptual argument.

- On pairs
`finset`

s, I added an explicit induction. - On
`topological_space`

, I added a general lemma that to show separation of`finset`

s it suffices to show separation of singletons. - Finally, the
`t2_space`

assumption is all that is needed to show the required separation!

#### Patrick Massot (Dec 16 2020 at 09:29):

@Damiano Testa I don't even see `disjoint_finsets_opens_of_t2`

in the current state of the PR.

#### Patrick Massot (Dec 16 2020 at 11:47):

As pointed out by Johan, I think the definition `separate`

doesn't make sense. You should have removed the disjointness assumption from there and move it to the main lemma. And if we need that definition at all then it should be about any sets, not only finite ones. That said I don't think we need it now. You can state your end goal as

```
lemma t2_separation_finsets [t2_space α] {s t : finset α} (h : s ∩ t = ∅) :
∃ U V : set α, is_open U ∧ is_open V ∧ ↑s ⊆ U ∧ ↑t ⊆ V ∧ U ∩ V = ∅
```

#### Patrick Massot (Dec 16 2020 at 11:47):

And I think it's worth the trouble of also stating the intermediate lemma

```
lemma t2_separation_point_finset [t2_space α] {s : finset α} {x : α} (h : x ∉ s) :
∃ U V : set α, is_open U ∧ is_open V ∧ ↑s ⊆ U ∧ x ∈ V ∧ U ∩ V = ∅ :=
```

since it makes sense to know it independently.

#### Patrick Massot (Dec 16 2020 at 11:48):

I think you are right that they key is to have relevant induction lemmas for finsets. But I think the one you chose is not the most relevant one.

#### Patrick Massot (Dec 16 2020 at 11:49):

The key feature of these topological lemmas is they are about disjoint points and finsets. So I propose to prove:

```
lemma finset.induction_disjoint_point {α : Type*} {P : α → finset α → Prop} {x : α}
(h : P x ∅) (hrec : ∀ y s, x ≠ y → P x s → P x (insert y s)) : ∀ s, x ∉ s → P x s
lemma finset.induction_disjoint {α : Type*} {P : finset α → finset α → Prop} {s : finset α}
(h : P s ∅) (hrec : ∀ x t, x ∉ s → P s t → P s (insert x t)) : ∀ t, s ∩ t = ∅ → P s t
```

which should be straightforward applications of `finset.induction_on`

.

#### Patrick Massot (Dec 16 2020 at 11:50):

and then use them to prove the two topological lemmas (the second topological lemma using the first one of course).

#### Patrick Massot (Dec 16 2020 at 11:53):

Do you want help or are you still happy to learn stuff using this example?

#### Damiano Testa (Dec 16 2020 at 13:38):

Ah, I found out now your comments here, but I just pushed a new version. I will now read and merge your comments!

#### Damiano Testa (Dec 16 2020 at 13:41):

I am happy to try your suggestion out. Should you find that pointing me in the right direction becomes more work for you than to simply do it yourself, please say so!

#### Damiano Testa (Dec 16 2020 at 13:44):

One quick question: I am happy to go with either `disjoint a b`

or `a ∩ b = ∅`

.

Is there any particular reason to prefer one over the other?

#### Kevin Buzzard (Dec 16 2020 at 13:45):

One should prefer the version which shows up more in mathlib -- this will be the version deemed "canonical", so the one which the simp lemmas will mention etc

#### Kevin Buzzard (Dec 16 2020 at 13:48):

a regexp search for `.* ∩ .* = ∅`

gives only three hits, and `disjoint`

has 99 hits

#### Kevin Buzzard (Dec 16 2020 at 13:50):

```
import tactic
example (X : Type) (s t : set X) : disjoint s t ↔ ∀ {a}, a ∈ t → a ∉ s :=
begin
library_search -- works
end
example (X : Type) (s t : set X) : s ∩ t = ∅ ↔ ∀ {a}, a ∈ t → a ∉ s :=
begin
library_search -- fails
end
```

I would use `disjoint`

.

#### Damiano Testa (Dec 16 2020 at 13:51):

Ok, I will keep `disjoint`

, then!

#### Patrick Massot (Dec 16 2020 at 15:14):

Damiano Testa said:

Should you find that pointing me in the right direction becomes more work for you than to simply do it yourself, please say so!

This is not at all how I see it. I claim it's important that many mathematicians learn how to use a proof assistant, with the distant goal that one day proof assistants will be useful tools for mathematics. Hence I'm happy to spend some time helping other mathematicians to learn. My goal here isn't to get more lemmas about T2 spaces into mathlib as quickly as possible.

#### Patrick Massot (Dec 16 2020 at 15:17):

Looking at the latest version of the PR, I see that using your union induction principle is actually quite efficient, so maybe I was wrong about the most relevant induction lemmas here. I still claim:

- my two induction principles for finsets could be useful, so it would be nice to have them
- you should define
`separate`

for arbitrary sets, and maybe rename it to`separated`

, the current version sounds grammatically weird (but I'm not a native speaker)

#### Patrick Massot (Dec 16 2020 at 15:18):

- The version where one point is separated from a finset is also worth spelling out (you can deduce it from the version separating two finsets of course)

#### Patrick Massot (Dec 16 2020 at 15:22):

I have another exercise for you, related to your proof and a question you asked recently. I see from your proofs that we have a lemma `is_open_union`

, that you use as `is_open_union oU oW`

. This is a waste of typing. It should be `oU.union oW`

which is shorter and looks nice. It means someone needs to rename `is_open_union`

to `is_open.union`

and then fix mathlib, enjoying all the shorten proofs on the way. The same holds for `is_open_inter`

, `is_closed_union`

and `is_closed_inter`

. This can be a separate PR. The main goal here is to increase your understanding of the dot notation magic.

#### Patrick Massot (Dec 16 2020 at 15:24):

Kevin Buzzard said:

a regexp search for

`.* ∩ .* = ∅`

gives only three hits, and`disjoint`

has 99 hits

This means the definition of `t2_space`

and surrounding lemmas should change.

#### Damiano Testa (Dec 16 2020 at 16:11):

Dear Patrick,

I have finished the earlier exercise, here is a solution (the `_1`

in the names are an artifact, since I had them in the file `topology.separation`

and for the purpose of posting here, I wanted to make sure that I avoided circularity):

```
import topology.separation
open set
local attribute [instance] classical.prop_decidable
universes u
variables {α : Type u} [topological_space α]
lemma finset.induction_disjoint_point_1 {α : Type*} {P : α → finset α → Prop} {x : α}
(h : P x ∅) (hrec : ∀ y s, x ≠ y → P x s → P x (insert y s)) : ∀ s, x ∉ s → P x s :=
begin
refine λ s, finset.induction_on s (λ _, h) (λ a t ta iP xat, _),
apply hrec _ _ (by { rintro rfl, exact xat (finset.mem_insert_self _ t) }) (iP (λ _, _)),
exact xat (finset.mem_insert_of_mem _x),
end
lemma finset.induction_disjoint_1 {α : Type*} {P : finset α → finset α → Prop} {s : finset α}
(h : P s ∅) (hrec : ∀ x t, x ∉ s → P s t → P s (insert x t)) : ∀ t, disjoint s t → P s t :=
begin
refine λ t, finset.induction_on t (λ _, h) _,
refine λ a u au hP sau, hrec a u (finset.disjoint_insert_right.mp sau).1 (hP _),
exact finset.disjoint_of_subset_right (finset.subset_insert a u) sau,
end
lemma t2_separation_point_finset_1 [t2_space α] {s : finset α} {x : α} (h : x ∉ s) :
∃ U V : set α, is_open U ∧ is_open V ∧ ↑s ⊆ U ∧ x ∈ V ∧ U ∩ V = ∅ :=
begin
revert s,
refine finset.induction_disjoint_point _ (λ y s xy, _),
{ exact ⟨_, _, is_open_empty, is_open_univ, by refl, mem_univ x, inter_univ _⟩ },
{ rintros ⟨U, V, oU, oV, aU, bV, UV⟩,
obtain ⟨Uy, Vx, oUy, oVx, aUy, bVx, UyVx⟩ := t2_separation xy.symm,
refine ⟨U ∪ Uy, V ∩ Vx, is_open_union oU oUy, is_open_inter oV oVx, _, ⟨bV, bVx⟩, _⟩,
{ rw [finset.coe_insert, ← union_singleton, union_subset_iff],
refine ⟨subset_union_of_subset_left aU _,
subset_union_of_subset_right (set.singleton_subset_iff.mpr aUy) _⟩ },
{ rw [union_inter_distrib_right, ← set.inter_assoc, UV, set.empty_inter _, set.empty_union],
rw [set.inter_comm V _, ← set.inter_assoc, UyVx, set.empty_inter] } },
end
lemma t2_separation_finsets_1 [t2_space α] {t s : finset α} (h : disjoint s t) :
∃ U V : set α, is_open U ∧ is_open V ∧ ↑s ⊆ U ∧ ↑t ⊆ V ∧ U ∩ V = ∅ :=
begin
symmetry' at h,
revert h,
refine finset.induction_disjoint _ (λ y u yt, _) _,
{ exact ⟨_, _, is_open_empty, is_open_univ, by refl, subset_univ _, inter_univ _⟩ },
{ rintros ⟨U, V, oU, oV, aU, bV, UV⟩,
obtain ⟨Ut, Vy, oUt, oVy, aUt, bVy, UtVy⟩ := t2_separation_point_finset yt,
refine ⟨U ∪ Vy, V ∩ Ut, is_open_union oU oVy, is_open_inter oV oUt, _, _, _⟩,
{ rw [finset.coe_insert, ← union_singleton, union_subset_iff],
refine ⟨subset_union_of_subset_left aU _,
subset_union_of_subset_right (set.singleton_subset_iff.mpr bVy) U⟩ },
{ exact subset_inter_iff.mpr ⟨bV, aUt⟩ },
{ rw [union_inter_distrib_right, ← set.inter_assoc, UV, set.empty_inter _, set.empty_union],
rw [set.inter_comm V _, ← set.inter_assoc, set.inter_comm _ Ut, UtVy, set.empty_inter] } },
end
```

#### Damiano Testa (Dec 16 2020 at 16:13):

I was indeed going to say that this solution does not look prettier than what I had before, but I also have not polished it as much! By "proof irrelevance", I am tempted to maintain the older version, if you agree! Especially since it already develops a little API around `separate`

.

I will change the name `separate`

to `separated`

and make it take `set`

s instead of `finsets`

as inputs.

After that, I will read again your comments and see what else I missed!

#### Damiano Testa (Dec 16 2020 at 16:21):

I do run into the issue of converting a `finset`

into a `set`

: is there a standard way?

#### Eric Wieser (Dec 16 2020 at 16:23):

(deleted)

#### Damiano Testa (Dec 16 2020 at 16:25):

This seems to work:

```
(s : finset α), {a : α | a ∈ s}
```

#### Kevin Buzzard (Dec 16 2020 at 16:27):

There seems to be a coercion:

```
import tactic
example (α : Type)
(s : finset α) : set α := s
```

#### Damiano Testa (Dec 16 2020 at 16:28):

I tried with the uparrow, but it did not seem to work for me...

#### Kevin Buzzard (Dec 16 2020 at 16:28):

```
import tactic
example (α : Type*) (s : finset α) : set α := ↑s
```

#### Damiano Testa (Dec 16 2020 at 16:29):

Ah, if I tell Lean what Type it should have, it works! Thanks!

#### Damiano Testa (Dec 16 2020 at 16:29):

```
∀ (s t : finset α), disjoint s t → separated (s : set α) t :=
```

(Now separated takes `sets`

as inputs)

#### Mario Carneiro (Dec 16 2020 at 16:31):

You could also state this as a theorem about `finite`

sets

#### Mario Carneiro (Dec 16 2020 at 16:31):

if you don't use anything about the finset besides the fact that it coerces to set

#### Damiano Testa (Dec 16 2020 at 16:33):

Ah, I have always glossed over the distinction between `finsets`

and `finite`

. Maybe this is the time to correct this!

I am doing an `finset.induction_on`

, though: this feels like it will be a problem...

#### Mario Carneiro (Dec 16 2020 at 16:34):

you can probably use `finite.induction_on`

then

#### Mario Carneiro (Dec 16 2020 at 16:34):

Actually, it would be nice if you could prove this without induction, it will probably be a lot shorter

#### Damiano Testa (Dec 16 2020 at 16:36):

I initially wanted to directly define the intersections over all open sets given by the `t2_separation`

, but I had bad memories of using the `big_operators`

and opted for reducing everything to pairwise intersections/unions...

#### Damiano Testa (Dec 16 2020 at 16:36):

I can very well see that if I knew how to use the `big_operators`

, I could do this directly, instead of by induction...

#### Mario Carneiro (Dec 16 2020 at 16:36):

You don't need big ops here, this is a big union which uses the basic set library

#### Damiano Testa (Dec 16 2020 at 16:37):

in any case, with the coercion, it only occupies one more line than before!

#### Damiano Testa (Dec 16 2020 at 16:38):

Ah, I remember now: my issue was getting the "choice" function for the t2_separation on all pairs of points. That is what stumped me.

And I confess that, while I proved the lemmas that Patrick suggested earlier, I did not really understand the `option/get/some`

stuff...

#### Mario Carneiro (Dec 16 2020 at 16:39):

It might also be nice to have a version of the separation axiom that says that given `x, y`

distinct there is `x \in U`

such that `y \notin closure U`

#### Mario Carneiro (Dec 16 2020 at 16:39):

that means one less set to deal with

#### Mario Carneiro (Dec 16 2020 at 16:40):

You don't really need that here - since you are local to a single proof you can use the `choice`

tactic to make the function on the spot

#### Damiano Testa (Dec 16 2020 at 16:52):

As usual, I like your suggestions! However, I prefer to keep the PR as it is now and think about what else to add later. Does this seem reasonable?

#### Damiano Testa (Dec 16 2020 at 16:53):

(Btw, I also pushed the latest version of #5332. This version now has `separated`

instead of `separate`

and the inputs are two `sets`

instead of two `finsets`

. Everything else is essentially the same!)

#### Damiano Testa (Dec 16 2020 at 16:57):

Todo (as per Patrick's comment):

- add the two induction principles (probably a separate PR);
- add lemma for separating one point from a
`finset`

(this should be easy, but I may not have time to do it now: it might appear in the next iteration of this PR); - change
`is_open_union`

to`is_open.union`

and compress using projection notation. Similarly for`is_open_inter`

,`is_closed_union`

,`is_closed_inter`

(again, this is probably a separate PR).

#### Damiano Testa (Dec 16 2020 at 17:06):

Which of these two version is "better"? Does it make a difference?

```
lemma point_disjoint_finset_opens_of_t2 [t2_space α] {x : α} {s : finset α} (h : x ∉ s) :
separated (({x} : finset α) : set α) ↑s :=
finset_disjoint_finset_opens_of_t2 {x} s (singleton_disjoint.mpr h)
```

or

```
lemma point_disjoint_finset_opens_of_t2 [t2_space α] {x : α} {s : finset α} (h : x ∉ s) :
separated ({x} : set α) ↑s :=
begin
rw ← coe_singleton x,
exact finset_disjoint_finset_opens_of_t2 {x} s (singleton_disjoint.mpr h),
end
```

#### Mario Carneiro (Dec 16 2020 at 17:09):

Also consider

```
lemma point_disjoint_finset_opens_of_t2 [t2_space α] {x : α} {s : set α} (h : x ∉ s) (hf : finite s) :
separated {x} s := ...
```

#### Mario Carneiro (Dec 16 2020 at 17:11):

even better, prove that if `separated (s i) t`

for all `i`

, then `separated (\bigcup i, s i) t`

, and `separated`

is symmetric, without a `t2_space`

assumption

#### Mario Carneiro (Dec 16 2020 at 17:12):

Then, you can apply those two facts (and `separated {x} {y}`

in a `t2_space`

) to directly prove that finite sets are separated in a `t2_space`

#### Mario Carneiro (Dec 16 2020 at 17:13):

actually you should follow the lead of these topology theorems in your statement of finite unions and intersections:

```
lemma is_open_bInter {s : set β} {f : β → set α} (hs : finite s) :
(∀i∈s, is_open (f i)) → is_open (⋂i∈s, f i) :=
finite.induction_on hs
(λ _, by rw bInter_empty; exact is_open_univ)
(λ a s has hs ih h, by rw bInter_insert; exact
is_open_inter (h a (mem_insert _ _)) (ih (λ i hi, h i (mem_insert_of_mem _ hi))))
lemma is_closed_bUnion {s : set β} {f : β → set α} (hs : finite s) :
(∀i∈s, is_closed (f i)) → is_closed (⋃i∈s, f i) :=
finite.induction_on hs
(λ _, by rw bUnion_empty; exact is_closed_empty)
(λ a s has hs ih h, by rw bUnion_insert; exact
is_closed_union (h a (mem_insert _ _)) (ih (λ i hi, h i (mem_insert_of_mem _ hi))))
```

#### Damiano Testa (Dec 16 2020 at 17:15):

These lemmas are already in the PR: mathematically, they seem equivalent to what you are saying, right?

```
@[symm] lemma symm {s t : set α} : separated s t → separated t s :=
lemma union_left {a b c : set α} : separated a c → separated b c → separated (a ∪ b) c :=
```

#### Mario Carneiro (Dec 16 2020 at 17:15):

the first one yes, the second one not quite

#### Damiano Testa (Dec 16 2020 at 17:16):

(the assumptions are that alpha is a topological space, no t2 assumption)

#### Mario Carneiro (Dec 16 2020 at 17:16):

I mean the left side should be a finite union

#### Mario Carneiro (Dec 16 2020 at 17:16):

not a binary union

#### Damiano Testa (Dec 16 2020 at 17:16):

Ok, I replaced the finite union by the finset.induction part...

#### Mario Carneiro (Dec 16 2020 at 17:17):

As the two topology proofs show, it should not be more than a few lines to get from the binary version to the finite union version

#### Damiano Testa (Dec 16 2020 at 17:17):

In any case, it is now time for me to get to my "life outside Lean"! I will take a look at what happens here later!

Thank you very much!

#### Kevin Buzzard (Dec 16 2020 at 17:29):

There is life outside Lean??

Last updated: May 16 2021 at 05:21 UTC