instContinuousInvMulOpposite — Mathlib

English

If a type α carries a group structure with a continuous inverse, then the opposite type αᵐᵒᵖ also carries a continuous inverse, i.e., inversion is continuous in the opposite

Русский

Если у типа α есть структура группы с непрерывной инверсией, то противоположный тип αᵐᵒᵖ также имеет непрерывную инверсию.

LaTeX

$$$ContinuousInv(\alpha^{\mathrm{op}})$$$

Lean4

@[to_additive]
instance [Inv α] [ContinuousInv α] : ContinuousInv αᵐᵒᵖ :=
  opHomeomorph.symm.isInducing.continuousInv unop_inv

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