α : Type u
β : Type v
γ : Type ?u.140260
δ : Type ?u.140263
ε : Type ?u.140266
ζ : Type ?u.140269
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsOpen (range inr)
α : Type u
β : Type v
γ : Type ?u.140260
δ : Type ?u.140263
ε : Type ?u.140266
ζ : Type ?u.140269
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsClosed (range inl)
rw [← isOpen_compl_iff, compl_range_inl]
no goals
α : Type u
β : Type v
γ : Type ?u.140260
δ : Type ?u.140263
ε : Type ?u.140266
ζ : Type ?u.140269
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsOpen (range inr)
exact isOpen_range_inr