coinduced_symm — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem coinduced_symm {α β : Type*} (e : α ≃ β) : TopologicalSpace.coinduced e.symm = TopologicalSpace.induced e :=
  e.symm.induced_symm.symm

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