toExistsAddOfLE — Mathlib

English

In a StarOrderedRing, a is nonnegative iff a lies in the closure of the set {star s · s}.

Русский

В StarOrderedRing элемент a неотрицателен тогда и только тогда, когда он лежит в замыкании множества {star s · s}.

LaTeX

$$$0 \\le a \\\\Leftrightarrow a \\\\in \\mathrm{closure}(\\\\{ star(s) \\cdot s \\\\mid s \\\\in R \\\\}).$$$

Lean4

instance (priority := 100) toExistsAddOfLE : ExistsAddOfLE R where
  exists_add_of_le
    h :=
    match (le_iff _ _).mp h with
    | ⟨p, _, hp⟩ => ⟨p, hp⟩

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