unitsLift_apply_inv_apply — Mathlib

English

For f : C(X, Mˣ), the inverse under the units-lift corresponds pointwise to the inverse in M: (unitsLift f)⁻¹(x) = f(x)⁻¹.

Русский

Для f : C(X, Mˣ) противоречиво: обратное отображение через подъем единиц даёт точно f(x)⁻¹ в точке x.

LaTeX

$$$\forall x,\ (\mathrm{unitsLift}(f))^{-1}(x) = f(x)^{-1}.$$$

Lean4

@[to_additive (attr := simp)]
theorem unitsLift_apply_inv_apply (f : C(X, Mˣ)) (x : X) : (↑(ContinuousMap.unitsLift f)⁻¹ : C(X, M)) x = (f x)⁻¹ :=
  rfl

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