α : Type u
β : Type v
γ : Type ?u.140501
δ : Type ?u.140504
ε : Type ?u.140507
ζ : Type ?u.140510
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsOpen (range inl)
α : Type u
β : Type v
γ : Type ?u.140501
δ : Type ?u.140504
ε : Type ?u.140507
ζ : Type ?u.140510
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsClosed (range inr)
rw [← isOpen_compl_iff, compl_range_inr]
no goals
α : Type u
β : Type v
γ : Type ?u.140501
δ : Type ?u.140504
ε : Type ?u.140507
ζ : Type ?u.140510
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
⊢ IsOpen (range inl)
exact isOpen_range_inl