coe_inv — Mathlib

English

For Inv β and ContinuousInv β, the evaluation of the inverse map is pointwise: for f ∈ C(α,β) and x ∈ α, (f⁻¹)(x) = (f(x))⁻¹.

Русский

Пусть β имеет обратное и непрерывную инверсию; тогда значение обратного отображения в точке равно обратному значению отображения: (f⁻¹)(x) = (f(x))⁻¹.

LaTeX

$$$\forall f:\ C(\alpha,\beta),\forall x:\ \alpha:\ (f^{-1})(x) = (f(x))^{-1}.$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_inv [Inv β] [ContinuousInv β] (f : C(α, β)) : ⇑f⁻¹ = (⇑f)⁻¹ :=
  rfl

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