α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set α), s ∈ B → IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (f '' o)
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
⊢ IsOpenMap f ↔ ∀ (s : Set α), s ∈ B → IsOpen (f '' s)
refine' ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => _⟩
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set α), s ∈ B → IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (⋃ (i : ↑{s | s ∈ B ∧ s ⊆ o}), f '' ↑i)
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set α), s ∈ B → IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (f '' o)
rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]
no goals
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set α), s ∈ B → IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (⋃ (i : ↑{s | s ∈ B ∧ s ⊆ o}), f '' ↑i)
exact isOpen_iUnion fun s => hf s s.2.1