orderedSub — Mathlib

English

The finsupp type ι →₀ α inherits an OrderedSub structure from the pointwise order, i.e., for all f,g,h : ι →₀ α, if f ≤ g then f - h ≤ g - h.

Русский

Тип FinSupp ι →₀ α наследует структуру OrderedSub, то есть для всех f,g,h : ι →₀ α, если f ≤ g, то f - h ≤ g - h.

LaTeX

$$$ \\forall f,g,h : ι \\to_0 α,\; f \\le g \\Rightarrow f - h \\le g - h $$$

Lean4

instance orderedSub : OrderedSub (ι →₀ α) :=
  ⟨fun _n _m _k => forall_congr' fun _x => tsub_le_iff_right⟩

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