open sets are unions of basis elements

Stream: maths

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

At its heart though is a triviality.

[Kevin Buzzard]

mem_basis_subset_of_mem_open says

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

instead of choosing one of them, choose all of them

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

proving that determinant is multiplicative (not in Lean)

[Kevin Buzzard]

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

[Kevin Buzzard]

so there are some interfaces if you need them

[Kenny Lau]

well you didn't use them

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

that's not true

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and I wanted a map sending i to x

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Kevin Buzzard]

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)

[Kevin Buzzard]

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.

[Kevin Buzzard]

i.e. I started by writing

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

Kenny can you write a proof in term mode?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I just wrote the first proof I thought of

[Kevin Buzzard]

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

[Mario Carneiro]

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)

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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