sum.inl is an open map

Stream: Is there code for X?

[Kevin Buzzard]

Is there a one-liner for this? I can't find it in mathlib and there are people around here who know this part of the library back to front.

import topology.constructions

/-
import contains

instance [t₁ : topological_space α] [t₂ : topological_space β] : topological_space (α ⊕ β) :=
coinduced sum.inl t₁ ⊔ coinduced sum.inr t₂

-/
lemma sum.inl_is_open_map {X Y : Type*} [topological_space X] [topological_space Y] :
  is_open_map (sum.inl : X → X ⊕ Y) := sorry

[Adam Topaz]

This should follow from docs#is_open_sum_iff right?

[Adam Topaz]

Oh docs#embedding_inl

[Adam Topaz]

docs#is_open_range_inl

[Adam Topaz]

Lol docs#open_embedding_inl

[Kevin Buzzard]

I might just come back in two minutes when you've finished ;-)

[Adam Topaz]

I'm on my phone and every time I click a link to find the next lemma even more useful

[Kevin Buzzard]

I've got it now -- thanks

[Kevin Buzzard]

in return I can offer you a sorry-free disjoint_union file in LTE :D

[Kevin Buzzard]

yeah I just missed those, sorry for wasting your time. I don't know the topology part of the library well.