induced_symm — Mathlib

English

For an equivalence e: α ≃ β, the topology induced by e.symm equals the topology coinduced by e: induced e.symm = coinduced e.

Русский

Для эквивалентности e: α ≃ β топология, индуцированная e^{-1} совпадает с коиндуцированной e: induced e^{-1} = coinduced e.

LaTeX

$$$\operatorname{induced} e^{-1} = \operatorname{coinduced} e$$$

Lean4

theorem induced_symm {α β : Type*} (e : α ≃ β) : TopologicalSpace.induced e.symm = TopologicalSpace.coinduced e :=
  by
  ext t U
  rw [isOpen_induced_iff, isOpen_coinduced]
  simp only [e.symm.preimage_eq_iff_eq_image, exists_eq_right, ← preimage_equiv_eq_image_symm]

Похожие утверждения