instNontrivialSubtypeLeOfNatOfAddLeftMono

English

Under suitable hypotheses (Nontrivial α, AddGroup α, LinearOrder α, AddLeftMono α), the nonnegative subtype is nontrivial.

Русский

При подходящих гипотезах (Nontrivial α, AddGroup α, LinearOrder α, AddLeftMono α) подтип неотрицательных элементов не тривиален.

LaTeX

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

Lean4

instance [Nontrivial α] [AddGroup α] [LinearOrder α] [AddLeftMono α] : Nontrivial { x : α // 0 ≤ x } :=
  by
  have ⟨a, ha⟩ := exists_ne (0 : α)
  obtain lt | lt := ha.lt_or_gt
  · exact ⟨0, ⟨-a, neg_nonneg.mpr lt.le⟩, Subtype.coe_ne_coe.mp (neg_ne_zero.mpr ha).symm⟩
  · exact ⟨0, ⟨a, lt.le⟩, Subtype.coe_ne_coe.mp ha.symm⟩

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