unitsOfForallIsUnit — Mathlib

English

Equivalence between continuous maps into units and units of continuous maps, realized by unitsLift, with coherence between forward and inverse directions.

Русский

Эквивалентность между непрерывными отображениями в единицы и единицами непрерывных отображений реализуется через построение unitsLift.

LaTeX

$$$C(X, M^{\times}) \cong \mathrm{Units}(C(X, M)).$$$

Lean4

/-- Construct a continuous map into the group of units of a normed ring from a function into the
normed ring and a proof that every element of the range is a unit. -/
@[simps]
noncomputable def unitsOfForallIsUnit {f : C(X, R)} (h : ∀ x, IsUnit (f x)) : C(X, Rˣ)
    where
  toFun x := (h x).unit
  continuous_toFun := continuous_isUnit_unit h

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