Zulip Chat Archive

Stream: Is there code for X?

Topic: disjoint_nhds_finite_of_t2


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!)

view this post on Zulip 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>

view this post on Zulip Mario Carneiro (Dec 11 2020 at 09:19):

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

view this post on Zulip Damiano Testa (Dec 11 2020 at 09:20):

Thanks for the suggestion: I will try!

view this post on Zulip 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)

view this post on Zulip 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 = )

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Dec 11 2020 at 10:56):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Dec 11 2020 at 10:58):

And it misses two lemmas saying both sets are open.

view this post on Zulip Patrick Massot (Dec 11 2020 at 10:58):

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

view this post on Zulip 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

view this post on Zulip Damiano Testa (Dec 11 2020 at 11:01):

Let me give it a try! Thanks!

view this post on Zulip Patrick Massot (Dec 11 2020 at 11:01):

Note that all proofs are two to four lines long.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:33):

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

view this post on Zulip Damiano Testa (Dec 11 2020 at 11:33):

Ah, I will try! Thanks!

view this post on Zulip 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)!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 = ∅)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Patrick Massot (Dec 11 2020 at 13:06):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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).

view this post on Zulip Damiano Testa (Dec 11 2020 at 13:08):

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

view this post on Zulip Patrick Massot (Dec 11 2020 at 13:08):

I mean disjoint_t2_open₁_t2_open₂

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Dec 11 2020 at 13:10):

I say make it 2 lines long now.

view this post on Zulip Damiano Testa (Dec 11 2020 at 13:10):

Ah, ok!

view this post on Zulip Damiano Testa (Dec 11 2020 at 13:11):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Dec 11 2020 at 13:13):

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

view this post on Zulip Patrick Massot (Dec 11 2020 at 13:14):

I should really work now instead of playing with Lean.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:32):

.

view this post on Zulip 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:

view this post on Zulip 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 )

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip Adam Topaz (Dec 12 2020 at 06:03):

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

view this post on Zulip Damiano Testa (Dec 12 2020 at 06:33):

Done!
#5332

Let's see if Lean also likes it!

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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 = 

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Dec 16 2020 at 11:53):

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

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 13:48):

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

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Dec 16 2020 at 13:51):

Ok, I will keep disjoint, then!

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Dec 16 2020 at 16:23):

(deleted)

view this post on Zulip Damiano Testa (Dec 16 2020 at 16:25):

This seems to work:

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

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 16:27):

There seems to be a coercion:

import tactic

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

view this post on Zulip Damiano Testa (Dec 16 2020 at 16:28):

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

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 16:28):

import tactic

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

view this post on Zulip Damiano Testa (Dec 16 2020 at 16:29):

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

view this post on Zulip Damiano Testa (Dec 16 2020 at 16:29):

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

(Now separated takes sets as inputs)

view this post on Zulip Mario Carneiro (Dec 16 2020 at 16:31):

You could also state this as a theorem about finite sets

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Dec 16 2020 at 16:34):

you can probably use finite.induction_on then

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Damiano Testa (Dec 16 2020 at 16:37):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 16:39):

that means one less set to deal with

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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!)

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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 := ...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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) :
  (is, is_open (f i))  is_open (is, 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) :
  (is, is_closed (f i))  is_closed (is, 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))))

view this post on Zulip 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 :=

view this post on Zulip Mario Carneiro (Dec 16 2020 at 17:15):

the first one yes, the second one not quite

view this post on Zulip Damiano Testa (Dec 16 2020 at 17:16):

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 17:16):

I mean the left side should be a finite union

view this post on Zulip Mario Carneiro (Dec 16 2020 at 17:16):

not a binary union

view this post on Zulip Damiano Testa (Dec 16 2020 at 17:16):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 17:29):

There is life outside Lean??


Last updated: May 16 2021 at 05:21 UTC