ι : Type ?u.27267
α : Type u_1
β : Type ?u.27273
γ : Type ?u.27276
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U V : Opens α
i : U ≤ V
⊢ IsOpen {x | ↑x ∈ ↑U}
ι : Type ?u.27267
α : Type u_1
β : Type ?u.27273
γ : Type ?u.27276
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U V : Opens α
i : U ≤ V
⊢ IsOpen (range (inclusion (_ : ↑U ⊆ ↑V)))
rw [Set.range_inclusion i]
no goals
ι : Type ?u.27267
α : Type u_1
β : Type ?u.27273
γ : Type ?u.27276
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U V : Opens α
i : U ≤ V
⊢ IsOpen {x | ↑x ∈ ↑U}
exact U.isOpen.preimage continuous_subtype_val