case h.a.h.a
α✝ : Type ?u.26688
β✝ : Type ?u.26691
γ : Type ?u.26694
t✝ t₁ t₂ : TopologicalSpace α✝
t' : TopologicalSpace β✝
f : α✝ → β✝
g : β✝ → α✝
α : Type u_1
β : Type u_2
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ IsOpen U ↔ IsOpen U
α✝ : Type ?u.26688
β✝ : Type ?u.26691
γ : Type ?u.26694
t t₁ t₂ : TopologicalSpace α✝
t' : TopologicalSpace β✝
f : α✝ → β✝
g : β✝ → α✝
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ TopologicalSpace.induced ↑e.symm = TopologicalSpace.coinduced ↑e
ext t U
case h.a.h.a
α✝ : Type ?u.26688
β✝ : Type ?u.26691
γ : Type ?u.26694
t✝ t₁ t₂ : TopologicalSpace α✝
t' : TopologicalSpace β✝
f : α✝ → β✝
g : β✝ → α✝
α : Type u_1
β : Type u_2
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ (∃ t_1, IsOpen t_1 ∧ ↑e.symm ⁻¹' t_1 = U) ↔ IsOpen (↑e ⁻¹' U)
case h.a.h.a
α✝ : Type ?u.26688
β✝ : Type ?u.26691
γ : Type ?u.26694
t✝ t₁ t₂ : TopologicalSpace α✝
t' : TopologicalSpace β✝
f : α✝ → β✝
g : β✝ → α✝
α : Type u_1
β : Type u_2
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ IsOpen U ↔ IsOpen U
rw [isOpen_induced_iff, isOpen_coinduced]
no goals
case h.a.h.a
α✝ : Type ?u.26688
β✝ : Type ?u.26691
γ : Type ?u.26694
t✝ t₁ t₂ : TopologicalSpace α✝
t' : TopologicalSpace β✝
f : α✝ → β✝
g : β✝ → α✝
α : Type u_1
β : Type u_2
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ (∃ t_1, IsOpen t_1 ∧ ↑e.symm ⁻¹' t_1 = U) ↔ IsOpen (↑e ⁻¹' U)
simp only [e.symm.preimage_eq_iff_eq_image, exists_eq_right, ← preimage_equiv_eq_image_symm]