instLE — Mathlib

English

If Y is partially ordered, then the order on LocallyFinsuppWithin U Y is defined componentwise by the underlying functions: D1 ≤ D2 iff D1(x) ≤ D2(x) for all x.

Русский

Если Y имеет частичный порядок, то порядок на LocallyFinsuppWithin U Y задаётся по компонентам: D1 ≤ D2 тогда и только тогда, когда D1(x) ≤ D2(x) для всех x.

LaTeX

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

Lean4

instance [LE Y] [Zero Y] : LE (locallyFinsuppWithin U Y) where le := fun D₁ D₂ ↦ (D₁ : X → Y) ≤ D₂

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