lt_def — Mathlib

English

For D1, D2 in LocallyFinsuppWithin with a preorder on Y, D1 < D2 iff the underlying functions satisfy D1 < D2 pointwise.

Русский

Для D1, D2 в LocallyFinsuppWithin с предорядком на Y верно: D1 < D2 тогда и только тогда, когда D1(x) < D2(x) для всех x.

LaTeX

$$$D_1 < D_2 \\iff (D_1 : X \\to Y) < (D_2 : X \\to Y)$$$

Lean4

theorem lt_def [Preorder Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} : D₁ < D₂ ↔ (D₁ : X → Y) < (D₂ : X → Y) :=
  ⟨(·), (·)⟩

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