case h_open
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (u : Set (α ⊕ β)), u ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t → IsOpen u

case h_nhds
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (a : α ⊕ β) (u : Set (α ⊕ β)),
    a ∈ u → IsOpen u → ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ a ∈ v ∧ v ⊆ u
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t)
apply isTopologicalBasis_of_open_of_nhds
case h_open.inl.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set α
hw : w ∈ s
⊢ IsOpen ((fun u => Sum.inl '' u) w)

case h_open.inr.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set β
hw : w ∈ t
⊢ IsOpen ((fun u => Sum.inr '' u) w)
case h_open
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (u : Set (α ⊕ β)), u ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t → IsOpen u
rintro u (⟨w, hw, rfl⟩ | ⟨w, hw, rfl⟩)
no goals
case h_open.inl.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set α
hw : w ∈ s
⊢ IsOpen ((fun u => Sum.inl '' u) w)
exact openEmbedding_inl.isOpenMap w (hs.isOpen hw)
no goals
case h_open.inr.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set β
hw : w ∈ t
⊢ IsOpen ((fun u => Sum.inr '' u) w)
exact openEmbedding_inr.isOpenMap w (ht.isOpen hw)
case h_nhds.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inl x ∈ v ∧ v ⊆ u

case h_nhds.inr
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inr x ∈ v ∧ v ⊆ u
case h_nhds
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (a : α ⊕ β) (u : Set (α ⊕ β)),
    a ∈ u → IsOpen u → ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ a ∈ v ∧ v ⊆ u
rintro (x | x) u hxu u_open
case h_nhds.inl.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inl x ∈ v ∧ v ⊆ u
case h_nhds.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inl x ∈ v ∧ v ⊆ u
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
  hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1
no goals
case h_nhds.inl.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inl x ∈ v ∧ v ⊆ u
exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
  image_subset_iff.2 vu⟩
case h_nhds.inr.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
v : Set β
vs : v ∈ t
xv : x ∈ v
vu : v ⊆ Sum.inr ⁻¹' u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inr x ∈ v ∧ v ⊆ u
case h_nhds.inr
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inr x ∈ v ∧ v ⊆ u
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
  ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2
no goals
case h_nhds.inr.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
v : Set β
vs : v ∈ t
xv : x ∈ v
vu : v ⊆ Sum.inr ⁻¹' u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inr x ∈ v ∧ v ⊆ u
exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
  image_subset_iff.2 vu⟩