quasiSeparatedSpace_congr — Mathlib

English

Quasi-separatedness is invariant under homeomorphisms: α ≃ₜ β iff QuasiSeparatedSpace α ⇔ QuasiSeparatedSpace β.

Русский

Квазиразделимость сохраняется при биективном гомоморфизме: α ≃ₜ β эквивалентно QuasiSeparatedSpace α ⇔ QuasiSeparatedSpace β.

LaTeX

$$quasiSeparatedSpace_congr e : QuasiSeparatedSpace α ↔ QuasiSeparatedSpace β$$

Lean4

theorem quasiSeparatedSpace_congr (e : α ≃ₜ β) : QuasiSeparatedSpace α ↔ QuasiSeparatedSpace β
    where
  mp _ := .of_isOpenEmbedding e.symm.isOpenEmbedding
  mpr _ := .of_isOpenEmbedding e.isOpenEmbedding

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