disjoint_nhds_finite_of_t2

Stream: Is there code for X?

[Damiano Testa]

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]

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]

(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]

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

[Mario Carneiro]

and then use classical.some on this proof to get the function

[Damiano Testa]

Thanks for the suggestion: I will try!

[Mario Carneiro]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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]

And it misses two lemmas saying both sets are open.

[Patrick Massot]

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

[Patrick Massot]

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]

Let me give it a try! Thanks!

[Patrick Massot]

Note that all proofs are two to four lines long.

[Patrick Massot]

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]

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

[Damiano Testa]

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]

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]

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]

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]

I did identify the _ in the underscore as F, though! This is the only use that I have for the obtain line...

[Mario Carneiro]

Whenever you see a some, use some_spec with the same hypothesis given to some

[Damiano Testa]

Ah, I will try! Thanks!

[Damiano Testa]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

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]

Thanks for your proofs! I also had all the terms in the rcases ... ⟨_, _, _, D, _⟩ labeled, but then I dropped them, for obscurity!

[Patrick Massot]

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

[Damiano Testa]

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]

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]

Ok, now try to prove that next lemma in two lines (one rcases and one more line).

[Damiano Testa]

Seeing your proofs, I could probably avoid unfolding and separate the cases presciently...

[Patrick Massot]

I mean disjoint_t2_open₁_t2_open₂

[Damiano Testa]

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]

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

[Patrick Massot]

I say make it 2 lines long now.

[Damiano Testa]

Ah, ok!

[Damiano Testa]

(sorry, I was still processing the _ and -)

[Patrick Massot]

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]

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

[Patrick Massot]

I should really work now instead of playing with Lean.

[Patrick Massot]

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]

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]

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

[Eric Wieser]

.

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Adam Topaz]

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]

@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]

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]

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

[Damiano Testa]

Done!
#5332

Let's see if Lean also likes it!

[Damiano Testa]

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]

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]

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]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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]

@Damiano Testa I don't even see disjoint_finsets_opens_of_t2 in the current state of the PR.

[Patrick Massot]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Damiano Testa]

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]

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]

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]

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]

a regexp search for .* ∩ .* = ∅ gives only three hits, and disjoint has 99 hits

[Kevin Buzzard]

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]

Ok, I will keep disjoint, then!

[Patrick Massot]

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]

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]

• 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]

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]

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]

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]

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.

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

[Damiano Testa]

I do run into the issue of converting a finset into a set: is there a standard way?

[Eric Wieser]

(deleted)

[Damiano Testa]

This seems to work:

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

[Kevin Buzzard]

There seems to be a coercion:

import tactic

example (α : Type)
  (s : finset α) : set α := s

[Damiano Testa]

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

[Kevin Buzzard]

import tactic

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

[Damiano Testa]

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

[Damiano Testa]

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

(Now separated takes sets as inputs)

[Mario Carneiro]

You could also state this as a theorem about finite sets

[Mario Carneiro]

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

[Damiano Testa]

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]

you can probably use finite.induction_on then

[Mario Carneiro]

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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]

that means one less set to deal with

[Mario Carneiro]

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]

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]

(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]

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]

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]

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]

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]

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]

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]

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]

the first one yes, the second one not quite

[Damiano Testa]

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

[Mario Carneiro]

I mean the left side should be a finite union

[Mario Carneiro]

not a binary union

[Damiano Testa]

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

[Mario Carneiro]

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]

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]

There is life outside Lean??