Inv — Mathlib

English

An equivalence e : α ≃ β transfers inverse from β to α by defining inv x := e^{-1}( e x )^{-1}.

Русский

Эквивалентность e : α ≃ β переносит обратное из β на α через определение inv x := e^{-1}( e x )^{-1}.

LaTeX

$$$$\operatorname{Inv}_{\alpha} = e^{-1}\big( (e x)^{-1} \big).$$$$

Lean4

/-- Transfer `Inv` across an `Equiv` -/
@[to_additive /-- Transfer `Neg` across an `Equiv` -/
    ]
protected abbrev Inv [Inv β] : Inv α where inv x := e.symm (e x)⁻¹

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