instStarOrderedRing — Mathlib

English

The nonnegative real numbers ℝ≥0 carry a StarOrderedRing structure with the star being the identity.

Русский

Неотрицательные действительные числа ℝ≥0 образуют структуру звездоупорядоченного кольца, где операция звезды является тождественной.

LaTeX

$$$\exists *: \mathbb{R}_{\ge 0} \to \mathbb{R}_{\ge 0},\ \forall x \in \mathbb{R}_{\ge 0}, x^{*} = x$$$

Lean4

instance instStarOrderedRing : StarOrderedRing ℝ≥0 :=
  by
  refine .of_le_iff fun x y ↦ ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨d, rfl⟩ := exists_add_of_le h
    refine ⟨sqrt d, ?_⟩
    simp only [star_trivial, mul_self_sqrt]
  · rintro ⟨p, -, rfl⟩
    exact le_self_add

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