Why isn't there an existential here?

Stream: new members

[Callum Cassidy-Nolan]

Can I get some help with this proof ?

import topology.basic

theorem open_set_for_each
  (X : Type*)
  [topological_space X]
  (A : set X)
  (h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊂ A) :
  is_open A :=
begin
  have f : A → set X ,
  {
    intro a,
    let x := h₀ a,
    -- Trying to get my set U
  },
  -- have : A = ⋃ (i : A), f i :=
  -- {

  -- }
end

Pretty much I'm trying to build my function from A to set X by evaluating h0 at a point a, but I'm running into trouble because after let x : = h0 a my goal state is

X: Type u_1
_inst_1: topological_space X
A: set X
h₀: ∀ (x : X), x ∈ A → (∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊂ A)
a: ↥A
x: ↑a ∈ A → (∃ (U : set X), is_open U ∧ ↑a ∈ U ∧ U ⊂ A) := h₀ ↑a
⊢ set X

but I thought that x would have become ∃ (U : set X), is_open U ∧ ↑a ∈ U ∧ U ⊂ A and then I could use that set U...

[Patrick Massot]

Did you try suggest?

[Patrick Massot]

Also, you probably meant ⊆, not ⊂

[Patrick Massot]

As suggest will reveal, your lemma is a repackaging of docs#is_open_iff_forall_mem_open

[Patrick Massot]

If you feel this is cheating then you'll have to tell us more about the constraints in your game.

[Callum Cassidy-Nolan]

My goal is to prove it using the fact that the union of open sets is still open

[Callum Cassidy-Nolan]

So first I want to build that function f which takes an element of A and maps it to the U you would get from h0, then I'll take the union of that function over every i in A

[Callum Cassidy-Nolan]

But the goal state isn't like I expected.

[Ruben Van de Velde]

You'll want let f, not have, in any case

[Patrick Massot]

The first line you want is probably choose! f hf using h₀, then

[Ruben Van de Velde]

The problem you have seems to be related to the difference between sets and types in lean, though. I'd try let x := h\0 a _,, leaving a proof obligation for a \in A, and then simp or suggest will probably prove that

[Ruben Van de Velde]

But Patrick's suggestion will likely get you more than one step ahead :)

[Patrick Massot]

Something like:

begin
  choose! f hf using h₀,
  have : A = ⋃ x ∈ A, f x,
  {
    sorry },
  rw this,
  apply is_open_bUnion,
  sorry
end

[Patrick Massot]

I just read the code you actually pasted. There is no way you'll be able to construct data out of that existential without using choice. You can try and you'll get Lean complaining about only being able to eliminate into Prop.

[Patrick Massot]

You can try with

begin
  let f : A → set X ,
  { intro a,
    cases h₀ a a.property with U hU,

  },
  -- have : A = ⋃ (i : A), f i :=
  -- {

  -- }
end

[Patrick Massot]

And this introduces the subtype associated to A, which you should avoid whenever possible. Note how my version features no function defined only on A.

[Callum Cassidy-Nolan]

Thanks for showing me the choose tactic, I managed to get the proof!

import topology.basic

open set

theorem open_set_for_each
  (X : Type*)
  [topological_space X]
  (A : set X)
  (h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊆ A) :
  is_open A :=
begin
  choose! f hf using h₀,
  have : A = ⋃ x ∈ A, f x,
  {
    ext p,
    split,
    {
      intro hp,
      have hfp := hf p hp,
      rw mem_Union,
      use p,
      rw mem_Union,
      use hp,
      exact hfp.2.1,
    },
    {
      intro hp,
      rw mem_Union at hp,
      cases hp with i hi,
      rw mem_Union at hi,
      cases hi with hia hpfi,
      have x := hf i hia,
      exact x.2.2 hpfi,
    }
  },
  rw this,
  apply is_open_bUnion,
  intros i hi,
  exact (hf i hi).1,
end

[Callum Cassidy-Nolan]

Do you have any feedback to shorten the intermediate proof?

[Yaël Dillies]

You can use mem_Union₂ instead of mem_Union twice.

[Kyle Miller]

Here's a way to avoid choice:

theorem open_set_for_each
  (X : Type*)
  [topological_space X]
  (A : set X)
  (h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊆ A) :
  is_open A :=
begin
  have : A = ⋃ U (h : U ⊆ A ∧ is_open U), U,
  { ext p,
    simp only [mem_Union, exists_prop],
    split,
    { intro hp,
      rcases h₀ p hp with ⟨U, hU, hxU, hUA⟩,
      use [U, hUA, hU, hxU], },
    { rintro ⟨U, ⟨hUA, hU⟩, hpU⟩,
      exact hUA hpU, }, },
  rw this,
  apply is_open_bUnion,
  rintros U ⟨hU, hU'⟩,
  exact hU',
end

(If you're unfamiliar with docs#rintro and docs#rcases, they're ways to simplify strings of cases.)

[Kyle Miller]

(This is actually somewhat similar in spirit to the choice-ful and choice-free proofs of Theorem 1.4 of Andrej Bauer's Five stages of accepting constructive mathematics.)

[Callum Cassidy-Nolan]

Thanks seeing that way is nice too

[Patrick Massot]

Yes, I wanted to create the function that was requested but the lemma itself doesn't need choice of course.

[Callum Cassidy-Nolan]

I moved on to a new question

image.png

I tried to model it like some of the theorems I saw in the docs, but I'ts not completely working out here's what I've gotten to so far

theorem intersection_of_topologies
  (X : Type*)
  (ι : Sort*)
  [topological_space X]
  (f : ι → topological_space X) :
  topological_space ∩ x ∈ ι, f x :=
begin
  sorry
end

Although I know parts of it aren't written correctly...

[Patrick Massot]

Your conclusion doesn't mean anything (and I would be surprised if Lean accepts to parse it)

[Callum Cassidy-Nolan]

Yeah, I'm trying to figure out how to use this definition image.png

in the book, we're saying that this set (the intersection) is a topology on X. But I'm not quite sure how I would write that in terms of the type theory version...

[Patrick Massot]

import topology.basic

def intersection_of_topologies {X : Type*} {ι : Sort*}
  (f : ι → topological_space X) : topological_space X :=
{ is_open := λ s, ∀ i, (f i).is_open s,
  is_open_univ := sorry,
  is_open_inter := sorry,
  is_open_sUnion := sorry }

[Callum Cassidy-Nolan]

Doesn't the statement we're proving have to talk about f how could topological_space X represent "the intersection of the topologies is a topology"?

[Callum Cassidy-Nolan]

Wait with a goal of topological_space X we're constructing a topology right?

[Callum Cassidy-Nolan]

I'm still confused as to why we don't need to talk about the intersection in our goal though...

[Patrick Massot]

topological_space X is the type of topologies on X. A term having this type gathers the data of which sets are open with the proofs of the conditions these opens sets must satisfy.

[Patrick Massot]

If you really want to see the intersection sign then you can write

def intersection_of_topologies {X : Type*} {ι : Sort*}
  (f : ι → topological_space X) : topological_space X :=
{ is_open := λ s, s ∈ ⋂ i, {t | (f i).is_open t},
  is_open_univ := sorry,
  is_open_inter := sorry,
  is_open_sUnion := sorry }

[Patrick Massot]

and then start each proof with simp_rw [set.mem_Inter, set.mem_set_of_eq], to get back to my formulation.

[Callum Cassidy-Nolan]

Is this definition a proof that the intersection of the topologies is a topology?

[Callum Cassidy-Nolan]

I thought we would write theorem instead?

[Patrick Massot]

theorem would mean it has only proofs. Here we are combining data (is the first field) with proofs

[Reid Barton]

mathlib has no way to say that "T : set (set X) is a topology on X", other than by building a topological_space structure whose first component is T. In other words, there's no is_topology.

[Reid Barton]

Nothing fundamental about that, we just never needed it.

[Callum Cassidy-Nolan]

Ok, so we have no way of saying is_topology, but so then how do we show something is a topology?

[Reid Barton]

As shown above

[Callum Cassidy-Nolan]

So you make a definition?

[Mauricio Collares]

The three sorries in Patrick's example should be filled in with proofs that the family of open sets given in is_open satisfies the correct axioms

[Mauricio Collares]

So it's a structure definition with one data field (component?) and three proof fields

[Callum Cassidy-Nolan]

Ok, I think I'm understanding it a little better now, and this thing is_open : set α → Prop is a function which determines if something is open or not right?

[Patrick Massot]

Yes.

[Patrick Massot]

But you don't have to use mathlib's way if you only want to do exercises in topology. Nothing prevents you from writing

import topology.basic

open set

structure is_topology {X : Type*} (T : set (set X)) : Prop :=
(univ_op : univ ∈ T)
(inter_op : ∀ u v ∈ T, u ∩ v ∈ T)
(Union_op : ∀ S : set (set X), S ⊆ T → ⋃₀ S ∈ T)

and playing with it. But you won't have all the lemmas we have about topologies in mathlib.

[Callum Cassidy-Nolan]

So in our scenario our open sets are the ones which are open in all each of the topologies in the family, so that's why you're using ∀ i, (f i).is_open s right?

[Patrick Massot]

You don't even have to use precisely the same wording, you can use:

structure is_topology {X : Type*} (T : set (set X)) : Prop :=
(Inter_op : ∀ S : set (set X), S ⊆ T → finite S → ⋂₀ S ∈ T)
(Union_op : ∀ S : set (set X), S ⊆ T → ⋃₀ S ∈ T)

[Julian Berman]

Maybe glossary#bundled-vs-unbundled is briefly useful too

[Callum Cassidy-Nolan]

Thanks, I'm starting to understand this more - I had never done a proof like that yet so the examples help!