opHomeomorph — Mathlib

English

The map op: M → Mᵐᵒᵖ is a homeomorphism (with inverse unop).

Русский

Отображение op: M → Mᵐᵒᵖ является гомеоморфизмом (обратное unop).

LaTeX

$$$$ \mathrm{op} : M \to M^{\mathrm{op}} \text{ is a homeomorphism (with inverse } \mathrm{unop}). $$$$

Lean4

/-- `MulOpposite.op` as a homeomorphism. -/
@[to_additive (attr := simps!) /-- `AddOpposite.op` as a homeomorphism. -/
    ]
def opHomeomorph : M ≃ₜ Mᵐᵒᵖ where
  toEquiv := opEquiv
  continuous_toFun := continuous_op
  continuous_invFun := continuous_unop

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