Using definition of topology

Stream: new members

[Nicolò Cavalleri]

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]

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]

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

[Nicolò Cavalleri]

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]

intros s hs is a bad start, I think

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

induced commutes with ⊓ and respects composition, so then you're done

[Reid Barton]

in particular, your first step in each continuous proof should be to use continuous_iff_le_induced

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

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

[Nicolò Cavalleri]

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]

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

[Mario Carneiro]

Alternatively you can apply continuous_inf_dom_left and continuous_induced_dom and so on

[Alex J. Best]

#L8 links to line number 8

[Nicolò Cavalleri]

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?