# Zulip Chat Archive

## Stream: new members

### Topic: Topological bases

#### Emiel Lanckriet (Aug 10 2020 at 18:30):

I am trying to proof that if T' is finer than T iff for x in X and each element of the basis B with x in B, there is an element of the basis B' such that x in that element and the new element is a subset of the old one.

I have written this code, but have some trouble reconciling the is_open with the generated_from, I used the generated from instead of topological_space.is_topological_basis because I couldn't seem to specify a topology.

```
import topology.basic topology.bases topology.metric_space.basic topology.order
open_locale classical filter
open filter set topological_space
example {α} {B B' : set (set α)} {t t' : topological_space α}
(h : t = topological_space.generate_from B) (h' : t' = topological_space.generate_from B') :
t' ≤ t ↔ ∀ (x : α) (b ∈ B), x ∈ b → (∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b) :=
begin
split,
{
intros t'fint x b bB xb,
use b,
split,
{
rw [h, h'] at t'fint,
have r := t'fint b,
sorry
},
{
split, assumption, refl
},
},
{
intros h U u_open,
sorry
},
end
```

I get stuck at the first sorry where the relevant parts of the environment are:

```
r: (generate_from B).is_open b ≤ (generate_from B').is_open b
bB : b \in B
\| b \in B'
```

So, either I should find how to show `(generate_from B).is_open b`

given ` b \in B`

or how to formulate this better using topological_space.is_topological_basis.

#### Kevin Buzzard (Aug 10 2020 at 18:54):

I don't see why it should be true that if B is a bunch of sets and B' is another bunch of sets, and the topology generated by B' is finer than the topology generated by B, then B is a subset of B'. But this is the goal state at your first sorry:

```
α: Type ?
BB': set (set α)
tt': topological_space α
h: t = generate_from B
h': t' = generate_from B'
x: α
b: set α
bB: b ∈ B
xb: x ∈ b
t'fint: generate_from B' ≤ generate_from B
⊢ b ∈ B'
```

So you have made a wrong turn somewhere.

#### Kevin Buzzard (Aug 10 2020 at 18:56):

Just before your `use`

statement your tactic state is

```
α: Type ?
B B': set (set α)
t t': topological_space α
h: t = generate_from B
h': t' = generate_from B'
t'fint: t' ≤ t
x: α
b: set α
bB: b ∈ B
xb: x ∈ b
⊢ ∃ (b' : set α) (H : b' ∈ B'), x ∈ b' ∧ b' ⊆ b
```

#### Kevin Buzzard (Aug 10 2020 at 18:57):

and you tried the tactic `use b`

but we now see that this is over-optimistic. What is the maths proof of what you're trying to do?

#### Kevin Buzzard (Aug 10 2020 at 19:02):

PS why not just state your problem as

```
example {α} {B B' : set (set α)} :
(generate_from B' ≤ generate_from B) ↔ ∀ (x : α) (b ∈ B), x ∈ b → (∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b) :=
```

instead of introducing all those t's (actually the notation is pretty useful, maybe this isn't such a good idea)

#### Emiel Lanckriet (Aug 10 2020 at 19:08):

Ah, yes, indeed, I mistook the bases for the topologies.

#### Kevin Buzzard (Aug 10 2020 at 19:09):

```
example {α} {B B' : set (set α)} {t t' : topological_space α}
(h : t = topological_space.generate_from B) (h' : t' = topological_space.generate_from B') :
t' ≤ t ↔ ∀ (x : α) (b ∈ B), x ∈ b → (∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b) :=
begin
split,
{
intros t'fint x b bB xb,
have h2 : t'.is_open b,
{ apply t'fint,
rw h,
exact generate_open.basic b bB,
},
```

There's a start. This is a proof that b is open for the t' topology.

#### Kevin Buzzard (Aug 10 2020 at 19:12):

and perhaps the next three lines should be

```
rw h' at h2,
change generate_open B' b at h2,
induction h2 with AAA BBB CCC DDD EEE FFF GGG HHH III JJJ KKK LLL MMM,
```

where I use triple capital letters at first and then I go through looking at all the goals, and change the names of the variables to more appropriate names.

#### Kevin Buzzard (Aug 10 2020 at 19:15):

the thing about the topological space generated by a collection of sets is that the definition of the open sets is given recursively. `h2`

is a proof that something is an open set in the topology generated by B', and there are four ways that that can happen: either it's in B', or it's the whole space, or it's the intersection of two sets we already generated, or it's a union of sets we already generated. I don't know what your maths proof is but if you want to do it from first principles then perhaps you need this inductive step. Of course if you're prepared to use things from the library then it might be easier -- it might well already be in there for all I know.

#### Emiel Lanckriet (Aug 10 2020 at 19:20):

The maths proof is quite simple: So, take X \in X and b \in B, then b belongs to t and t \sub t', hence b \in t'. Since t' is generated by B', there is a b' \in B' such that x \in B' \sub B.

#### Emiel Lanckriet (Aug 10 2020 at 19:20):

This is the proof taken literally from the book, but of course the last step is harder in formalization.

#### Kevin Buzzard (Aug 10 2020 at 20:03):

So then maybe don't do this induction step. Can you give me more details about the claim "Since t' is generated by B', there is a b' \in B' such that x \in B' \sub B". This is your first mention of x, there was an X before, and you don't mention b' at all, so maybe you have some typos in your book? It would be good to find a sentence which makes sense and you can type into Lean, then we can see if we can (a) prove it and (b) use it.

#### Kevin Buzzard (Aug 10 2020 at 20:04):

Note that I did the first line of the proof in your book: I showed b was in t' (this is my `h2`

).

#### Patrick Massot (Aug 10 2020 at 20:46):

@Emiel Lanckriet what you are trying yo prove is wrong. There is a mismatch between definitions.

#### Patrick Massot (Aug 10 2020 at 21:16):

Let me now answer your actual question. You had trouble using `is_topological_basis`

because this predicate, like most of the library, is really meant to work with a single topology on a given type. In technical terms, the topological structure is inferred by a mechanism called "type class instance resolution" that works great but assumes there is only one instance of each class on a given type (this is a simplified story, but good enough for now). This instance resolution is part of *elaboration*, the process where the proof assistant tries to figure out all the information you didn't explicitly provided. The good news here is that you can always override this elaboration process by prefixing lemma or definition names with a `@`

and providing as much information as you want (using underscores for stuff you don't want to provide).

#### Patrick Massot (Aug 10 2020 at 21:17):

This doesn't give pretty code (lots of `@`

and `_`

), but it works.

#### Patrick Massot (Aug 10 2020 at 21:21):

If you still want an exercise, you can first copy the statements and try to prove it. If this is still difficult, you can also note that the relevant lemmas are `mem_basis_subset_of_mem_open`

, `is_open_of_is_topological_basis`

, `mem_basis_subset_of_mem_open`

(and `is_open_iff_forall_mem_open`

which has nothing to do with bases).

```
import topology.basic topology.bases topology.metric_space.basic topology.order
open_locale classical filter
open filter set topological_space
example {α : Type*} {B B' : set (set α)} {t t' : topological_space α}
(h : @is_topological_basis _ t B) (h' : @is_topological_basis _ t' B') :
t' ≤ t ↔ ∀ (x : α) (b ∈ B), x ∈ b → (∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b) :=
begin
split,
{ intros H x b b_in x_in,
apply mem_basis_subset_of_mem_open h' x_in _,
apply H,
exact @is_open_of_is_topological_basis _ t _ _ h b_in },
{ intros H b b_op,
change @is_open _ t' b,
rw @is_open_iff_forall_mem_open α b t',
intros x x_in,
rcases @mem_basis_subset_of_mem_open _ t _ h _ b x_in b_op with ⟨b₁, b₁_in, x_in₁, hb₁b⟩,
rcases H x _ b₁_in x_in₁ with ⟨b', b'_in, x_in_b', hb'b₁⟩,
exact ⟨b', subset.trans hb'b₁ hb₁b, @is_open_of_is_topological_basis α t' _ _ h' b'_in, x_in_b'⟩ },
end
```

#### Emiel Lanckriet (Aug 10 2020 at 21:38):

Thanks a lot, I'll take a look at it tomorrow. Right now I am trying to work my way through Topology by Munkres to familiarize with the formalization of topology. Are there better ways?

#### Emiel Lanckriet (Aug 10 2020 at 21:41):

Thanks, the proof is easy to understand intuitively, but formalizing it isn't always as easy. I still have the bad habit of kinda brute forcing the proof by just looking at the state after each step and ignoring my mathematical knowledge.

#### Patrick Massot (Aug 10 2020 at 21:44):

If you want to understand topology in mathlib you should rather read Bourbaki (or I M James).

#### Kevin Buzzard (Aug 10 2020 at 21:49):

Topology turns out to be slicker to formalise with filters than with manipulations of open sets, so many of the proofs in mathlib are done with filters.

#### Patrick Massot (Aug 10 2020 at 21:51):

Hopefully https://www.youtube.com/watch?v=hhOPRaR3tx0 can help a bit.

#### Emiel Lanckriet (Aug 11 2020 at 10:18):

Ah, yes, I already watched the video before, but I thought that it would be fruitfull to try to translate the things in Munkres to filters. But for this kind of proof the filters didn't seem to be present.

#### Emiel Lanckriet (Aug 11 2020 at 14:15):

To go on on the same topic, I am trying to proof that if Y is open in the topolgy on X and U is open on the subspace topology on Y then U is open on the topology on X. I have found the file topology.constructions which says that it has a subspace topology, but I can't find one.

#### Patrick Massot (Aug 11 2020 at 14:18):

This is docs#is_open.open_embedding_subtype_coe

#### Patrick Massot (Aug 11 2020 at 14:22):

Or even more directly docs#is_open.is_open_map_subtype_coe

#### Patrick Massot (Aug 11 2020 at 14:23):

```
import topology.constructions
example {X: Type*} [topological_space X] {Y : set X} (hY : is_open Y) {U : set Y} {hU : is_open U} :
is_open ((coe : Y → X) '' U) :=
hY.is_open_map_subtype_coe U hU
```

#### Patrick Massot (Aug 11 2020 at 14:23):

All the difficulty here is in understand `set`

and `subtype`

. See topology exercises in the lftcm2020 repository.

#### Emiel Lanckriet (Aug 11 2020 at 14:26):

Thanks a lot, I already looked at lftcm2020 about topology, but I clearly don't understand it all yet.

#### Patrick Massot (Aug 11 2020 at 14:26):

I mean doing the exercises, not only watching the intro video.

#### Patrick Massot (Aug 11 2020 at 14:26):

And yes, it's not easy.

#### Emiel Lanckriet (Aug 11 2020 at 14:30):

No, I mean I have done the exercises a few days ago, but I might take a look at them again, because I feel I didn't get it all and had to peek at the solution a lot.

Last updated: May 11 2021 at 13:22 UTC