Theorem: isOpen_swap (Ray/Misc/Prod.lean)

State before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
s : Set (A × B)
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ IsOpen s → IsOpen (swap '' s)
Tactic:
rw [Set.image_swap_eq_preimage_swap]
State after:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
s : Set (A × B)
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ IsOpen s → IsOpen (swap ⁻¹' s)

State before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
s : Set (A × B)
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ IsOpen s → IsOpen (swap ⁻¹' s)
Tactic:
exact IsOpen.preimage continuous_swap
State after:
no goals