le_def — Mathlib

English

The order relation on locally finitely supported functions coincides with the pointwise order of the underlying functions.

Русский

Порядок на локальнофинсупп совпадает с точечным порядком соответствующих функций.

LaTeX

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

Lean4

theorem le_def [LE Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} : D₁ ≤ D₂ ↔ (D₁ : X → Y) ≤ (D₂ : X → Y) :=
  ⟨(·), (·)⟩

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