le_iff' — Mathlib

English

If f has support contained in a finite set s, then f ≤ g if and only if f(i) ≤ g(i) for every i in s.

Русский

Если опора f содержится в конечном множестве s, то f ≤ g тогда и только тогда, когда f(i) ≤ g(i) для каждого i ∈ s.

LaTeX

$$If $\\,f.\\mathrm{support} \\subseteq s$, then $f \\le g \\iff \\forall i \\in s,\ f(i) \\le g(i).$$$

Lean4

theorem le_iff' (hf : f.support ⊆ s) : f ≤ g ↔ ∀ i ∈ s, f i ≤ g i :=
  ⟨fun h s _ ↦ h s, fun h s ↦ if H : s ∈ f.support then h s (hf H) else (notMem_support_iff.1 H).symm ▸ zero_le (g s)⟩

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