Zulip Chat Archive

Stream: maths

Topic: open sets are unions of basis elements


view this post on Zulip Kevin Buzzard (May 13 2018 at 11:30):

import analysis.topology.topological_space
open topological_space
universe u

lemma union_basis_elemnts_of_open {α : Type u} [topological_space α]
{B : set (set α)} (HB : is_topological_basis B) {U : set α} (HU : is_open U) :
 (β : Type u) (f : β  set α), U = set.Union f   i : β, f i  B :=
begin
  let β := {x : α // x  U},
  existsi β,
  let f0 := λ i : β, (mem_basis_subset_of_mem_open HB U i.property HU),
  let f := λ i, classical.some (f0 i),
  let f1 :  (i : β),  (H : (f i)  B), (i.val  (f i)  (f i)  U) := λ i, classical.some_spec (f0 i),
  let g := λ i, classical.some (f1 i),
  let g1 :  (i : β), (i.val  f i  f i  U) := λ i, classical.some_spec (f1 i),
  existsi f,
  split,
  { rw set.subset.antisymm_iff,
    split,
    { intros y Hy,
      let i : β := y,Hy,
      existsi (f y,Hy),
      constructor,
        existsi i,
        refl,
      exact (g1 i).left,
    },
    { intros y Hy,
      cases Hy with V HV,cases HV with HV Hy,cases HV with i Hi,
      apply (g1 i).2,
      rwa Hi,
    },
  },
  { intro i,
    exact g i
  }
end

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:31):

That's the sort of proof I find very easy to write nowadays in tactic mode.

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:31):

At its heart though is a triviality.

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:31):

mem_basis_subset_of_mem_open says

view this post on Zulip Kenny Lau (May 13 2018 at 11:32):

you shouldn't use let for propositions (f0, f1, g1)

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:32):

for every element x of an open set U, there's some basis element V with x \in V and V \sub U

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:32):

So it's one of those things which is in some sense completely trivial

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:33):

however because I have to use classical arguments I find writing a one-liner very hard

view this post on Zulip Kenny Lau (May 13 2018 at 11:33):

also I don't think you need choice to do that, there's a trick I read somewhere

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:33):

So I just write it in tactic mode and I know I'll never get stuck

view this post on Zulip Kenny Lau (May 13 2018 at 11:33):

instead of choosing one of them, choose all of them

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:33):

Kenny what I care about is whether I should be concerned that I am writing this sort of proof in 30 lines of tactic mode

view this post on Zulip Kenny Lau (May 13 2018 at 11:34):

well I say that classical.some doesn't have a good interface

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:34):

and whether I should be striving to write a one-liner in term mode.

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:34):

Well I say that you are supposed to be sitting my exam at 10am tomorrow morning, so what are you doing chatting here? ;-)

view this post on Zulip Kenny Lau (May 13 2018 at 11:34):

proving that determinant is multiplicative (not in Lean)

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:35):

I talked about interface to classical.some recently and Simon wrote ccases and Mario wrote classical.rec_on

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:36):

so there are some interfaces if you need them

view this post on Zulip Kenny Lau (May 13 2018 at 11:36):

well you didn't use them

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:36):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/cases.20eliminating.20into.20type/near/125696468

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:37):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/cases.20eliminating.20into.20type/near/125695647

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:37):

I didn't use them because I have my own interface now -- see f,f1 and g,g1

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:38):

I don't really like it but it was easier to do it like that than find the thread

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:38):

that's not true

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:38):

I didn't use them because I didn't know how to use them in the middle of a function

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:38):

well, I didn't know how to use Simon's, and Mario's is in some sense just as complicated as what I did

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:39):

I was not in a situation where I had exists x, p x and I wanted x and H : p x

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:39):

I was in a situation where I wanted to construct a function

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:40):

so I had forall i, exists x, p i x

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:40):

and I wanted a map sending i to x

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:40):

hey, maybe I'm just saying that the interface for classical.some isn't great

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:41):

I guess I wanted a map sending i to x and a map sending i to a proof of p i x

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:41):

More precisely, I wanted a map f sending i to x and a map f_proof sending i to a proof of p i (f i)

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:42):

(rather than a proof of p i (classical.some _)

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:43):

and it still irks me a bit that I can't use a tactic which just builds these functions for me (with exactly those types, so no classical.some mentioned anywhere in the types, just in the definitions of the terms of these types)

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:43):

because my constructions of f f1 g and g1 involved building f, copying the type of the some_spec, editing it to replace classical.some _ with f i, then building f1, and this is a purely mechanical procedure.

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:45):

i.e. I started by writing

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:45):

  let f := λ i, classical.some (f0 i),
  let f1 := λ i, classical.some_spec (f0 i),

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:46):

and then I looked at the type of f1 in the context, edited it to remove all trace of classical.some (replacing it with f i) and then inserted the explicit type of f1.

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:46):

It somehow all feels like both a waste of time and something which students would find confusing.

view this post on Zulip Kevin Buzzard (May 13 2018 at 11:47):

Kenny can you write a proof in term mode?

view this post on Zulip Mario Carneiro (May 13 2018 at 12:10):

You shouldn't be using classical.some in the first place in this proof. It complicates things and there's no need. Before you start optimizing your use don't forget to see if another proof strategy works better by making canonical choices only

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:11):

I am a classical guy and have no feeling as to when I can get away with constructive maths

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:13):

I just wrote the first proof I thought of

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:14):

and I still find this sort of proof a joy to write

view this post on Zulip Mario Carneiro (May 13 2018 at 12:32):

I would go for the version with a set first:

lemma sUnion_basis_elemnts_of_open {α : Type u} [topological_space α]
{B : set (set α)} (HB : is_topological_basis B) {U : set α} (HU : is_open U) :
∃ (S : set (set α)), U = ⋃₀ S ∧ S ⊆ B :=
⟨{b ∈ B | b ⊆ U}, set.ext (λ a,
   ⟨λ ha, let ⟨b, hb, ab, bu⟩ := mem_basis_subset_of_mem_open HB _ ha HU in
              ⟨b, ⟨hb, bu⟩, ab⟩,
    λ ⟨b, ⟨hb, bu⟩, ab⟩, bu ab⟩),
 λ b h, h.1⟩

lemma Union_basis_elemnts_of_open {α : Type u} [topological_space α]
{B : set (set α)} (HB : is_topological_basis B) {U : set α} (HU : is_open U) :
∃ (β : Type u) (f : β → set α), U = (⋃ i, f i) ∧ ∀ i : β, f i ∈ B :=
let ⟨S, su, sb⟩ := sUnion_basis_elemnts_of_open HB HU in
⟨S, subtype.val, su.trans set.sUnion_eq_Union', λ ⟨b, h⟩, sb h⟩

(I didn't start out planning to write a term proof, but there never really came a point where I needed a tactic)

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:37):

Right -- I generally switch to tactic mode when I want to do something like a rw which I'm too lazy to figure out with the funny triangle thing. But here I switched because it just felt easier with the classical.stuff and I felt I'd been beaten too early, that was the reason I asked.

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:38):

I see the constructivist's trick now -- thanks.

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:39):

That was the idea I was missing -- I feel confident that I could have generated a term proof now.

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:40):

PS the mis-spelling of elements in the name was not intentional :-)

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:41):

I wanted to write "Union_of_basis_elements_of_open" but then I had two different ofs with two different meanings

view this post on Zulip Kevin Buzzard (May 13 2018 at 12:42):

PS1 is this already in mathlib? I couldn't find it. It is the canonical thing you do with a basis!

view this post on Zulip Reid Barton (May 13 2018 at 15:59):

I was in a situation where I wanted to construct a function
so I had forall i, exists x, p i x
and I wanted a map sending i to x

Use classical.axiom_of_choice

view this post on Zulip Reid Barton (May 13 2018 at 16:00):

@@ -11,6 +11,3 @@
   let f0 := λ i : β, (mem_basis_subset_of_mem_open HB U i.property HU),
-  let f := λ i, classical.some (f0 i),
-  let f1 : ∀ (i : β), ∃ (H : (f i) ∈ B), (i.val ∈ (f i) ∧ (f i) ⊆ U) := λ i, classical.some_spec (f0 i),
-  let g := λ i, classical.some (f1 i),
-  let g1 : ∀ (i : β), (i.val ∈ f i ∧ f i ⊆ U) := λ i, classical.some_spec (f1 i),
+  cases classical.axiom_of_choice f0 with f hf,
   existsi f,
@@ -25,3 +22,3 @@
         refl,
-      exact (g1 i).left,
+      exact (hf i).snd.1
     },
@@ -29,3 +26,3 @@
       cases Hy with V HV,cases HV with HV Hy,cases HV with i Hi,
-      apply (g1 i).2,
+      apply (hf i).snd.2,
       rwa ←Hi,
@@ -34,3 +31,3 @@
   { intro i,
-    exact g i
+    exact (hf i).fst
   }

view this post on Zulip Mario Carneiro (May 13 2018 at 16:01):

Oh yes, sorry for not engaging with the original question, Reid is right that you should use axiom_of_choice here


Last updated: May 11 2021 at 15:12 UTC