## 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.

#### 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: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:

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