sqrtHom — Mathlib

English

The function sqrtHom: ℝ≥0 →*₀ ℝ≥0 is a monoid-with-zero hom with sqrt, sqrt_zero, sqrt_one, sqrt_mul; i.e., it preserves multiplication and maps 0 to 0 and 1 to 1.

Русский

Функция sqrtHom: ℝ≥0 →*₀ ℝ≥0 является гомоморбом моноида с нулём: сохраняет умножение и отображает 0 в 0, 1 в 1.

LaTeX

$$$\forall a,b \in \mathbb{R}_{\ge 0},\ \sqrtHom(ab) = \sqrtHom(a)\sqrtHom(b) \land \sqrtHom(0)=0 \land \sqrtHom(1)=1$$$

Lean4

/-- `NNReal.sqrt` as a `MonoidWithZeroHom`. -/
noncomputable def sqrtHom : ℝ≥0 →*₀ ℝ≥0 :=
  ⟨⟨sqrt, sqrt_zero⟩, sqrt_one, sqrt_mul⟩

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