instWellFoundedGTWithZeroMultiplicativeIntLeOne

English

There is a well-founded greater-than relation on the set {v ∈ ℤᵐ⁰ | v ≤ 1}, i.e., no infinite descending chains.

Русский

Существует хорошо упорядоченная по отношению > структура на множество {v ∈ ℤᵐ⁰ | v ≤ 1}, то есть бесконечных нисходящих цепочек нет.

LaTeX

$$WellFoundedGT { v : ℤ^{\mathbf{m0}} // v ≤ 1 }$$

Lean4

instance instWellFoundedGTWithZeroMultiplicativeIntLeOne : WellFoundedGT { v : ℤᵐ⁰ // v ≤ 1 } :=
  {
    wf :=
      (LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero one_ne_zero).mpr
        instNonemptyOfInhabited }

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