## 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" somes 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 something

#### 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 1. I should pay more attention to the difference between - and _; 2. 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 unfolding 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 finsets having disjoint neighbourhoods... but not using somes... 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


.

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

1. On pairs finsets, I added an explicit induction.
2. On topological_space, I added a general lemma that to show separation of finsets it suffices to show separation of singletons.
3. 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: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 sets instead of finsets as inputs.

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

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

1. add the two induction principles (probably a separate PR);
2. 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);
3. 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