instIsSemirealOfIsStrictOrderedRingOfExistsAddOfLE

English

Let R be a semiring with a linear order such that for every a ≤ b there exists c with a + c = b (as in the natural numbers). Then R is semireal.

Русский

Пусть R — полукольцо с линейно упорядоченным отношением, удовлетворяющее свойству: для любых a ≤ b существует c, такое что a + c = b (например, в ℕ). Тогда R является семиреальным.

LaTeX

$$$(\text{Linearly ordered semiring } R \land (\forall a,b\in R, a \le b \Rightarrow \exists c\in R, a+c=b)) \Rightarrow IsSemireal(R)$$$

Lean4

/-- Linearly ordered semirings with the property `a ≤ b → ∃ c, a + c = b` (e.g. `ℕ`)
are semireal.
-/
instance [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] : IsSemireal R where
  one_add_ne_zero hs
    amo := zero_ne_one' R (le_antisymm zero_le_one (le_of_le_of_eq (le_add_of_nonneg_right hs.nonneg) amo))

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