nontrivial — Mathlib

English

If α is a semiring with linear order and IsStrictOrderedRing, then the nonnegative subtype is nontrivial.

Русский

Если α имеет линейное упорядочение и IsStrictOrderedRing, то подтип неотрицательных элементов не тривиален.

LaTeX

$$$\\text{Nontrivial}\\ { x : \\alpha \\mid 0 \\le x \\}$$$

Lean4

instance nontrivial [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] : Nontrivial { x : α // 0 ≤ x } :=
  ⟨⟨0, 1, fun h => zero_ne_one (congr_arg Subtype.val h)⟩⟩

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