# Zulip Chat Archive

## Stream: new members

### Topic: Using definition of topology

#### Nicolò Cavalleri (Oct 27 2020 at 19:23):

I don't know how can I tell lean "use the definition of this topology to prove this is open". How do I fill up the sorries here?

```
import topology.topological_fiber_bundle
variables (B : Type*) (F : Type*)
@[reducible] def weird_prod := Σ x : B, F
variables {B F}
def p1 : weird_prod B F → B := λ x, x.1
def p2 : weird_prod B F → F := λ x, x.2
instance [t₁ : topological_space B] [t₂ : topological_space F] :
topological_space (weird_prod B F) :=
topological_space.induced (p1) t₁ ⊓ topological_space.induced (p2) t₂
variables [topological_space B] [topological_space F]
def canonical_homeo : homeomorph (weird_prod B F) (B × F) :=
{ to_fun := λ x, ⟨x.fst, x.snd⟩,
inv_fun := λ y, ⟨y.fst, y.snd⟩,
left_inv := λ x, sigma.eq rfl rfl,
right_inv := λ x, prod.ext rfl rfl,
continuous_to_fun := by { intros s hs, dsimp, sorry },
continuous_inv_fun := by { sorry } }
```

#### Kevin Buzzard (Oct 27 2020 at 19:26):

What's the mathematical argument you're hoping to formalise here? If it's "it's obvious" then I'd be interested in some more details.

#### Reid Barton (Oct 27 2020 at 19:27):

"it's obvious" because https://github.com/leanprover-community/mathlib/blob/master/src/topology/constructions.lean#L51

#### Nicolò Cavalleri (Oct 27 2020 at 19:28):

Well the idea is that the two topologies are defined the same way so once I tell Lean how to translate one type into the other then the open sets are obviously the same

#### Reid Barton (Oct 27 2020 at 19:29):

`intros s hs`

is a bad start, I think

#### Kevin Buzzard (Oct 27 2020 at 19:29):

I'd be more tempted to check that some diagrams commuted first

#### Reid Barton (Oct 27 2020 at 19:29):

I'd start here: https://github.com/leanprover-community/mathlib/blob/master/src/topology/order.lean#L8

#### Reid Barton (Oct 27 2020 at 19:30):

`induced`

commutes with `⊓`

and respects composition, so then you're done

#### Reid Barton (Oct 27 2020 at 19:31):

in particular, your first step in each `continuous`

proof should be to use `continuous_iff_le_induced`

#### Kevin Buzzard (Oct 27 2020 at 19:32):

I guess the fact that p1 equals prod.fst o to_fun etc is definitional.

#### Reid Barton (Oct 27 2020 at 19:32):

right, the first thing you could try is `exact hs`

!

#### Reid Barton (Oct 27 2020 at 19:33):

this might work even though it seems like it obviously shouldn't

#### Nicolò Cavalleri (Oct 27 2020 at 19:33):

Reid Barton said:

I'd start here: https://github.com/leanprover-community/mathlib/blob/master/src/topology/order.lean#L8

Ok thanks can you tell me the name of the lemma you mean? Cause I can't manage to interpret #L8 and clicking the link for some reason brings me to the top of the page anyways

#### Reid Barton (Oct 27 2020 at 19:33):

I mean you should read the comment at the top of the page!

#### Mario Carneiro (Oct 27 2020 at 19:37):

Alternatively you can apply `continuous_inf_dom_left`

and `continuous_induced_dom`

and so on

#### Alex J. Best (Oct 27 2020 at 19:43):

#L8 links to line number 8

#### Nicolò Cavalleri (Oct 27 2020 at 19:54):

Reid Barton said:

`induced`

commutes with`⊓`

and respects composition, so then you're done

Doesn't it commute with `⊓`

only if the map is the same for the two induced?

Last updated: Dec 20 2023 at 11:08 UTC