le_iff' — Mathlib

English

If s contains f.support, then f ≤ g is equivalent to f(i) ≤ g(i) for all i ∈ s.

Русский

Пусть s содержит supp(f); тогда f ≤ g эквивалентно f(i) ≤ g(i) для всех i ∈ s.

LaTeX

$$Assume f.support ⊆ s. f ≤ g \iff \forall i ∈ s, f(i) ≤ g(i)$$

Lean4

theorem le_iff' (f g : ι →₀ α) {s : Finset ι} (hf : f.support ⊆ s) : f ≤ g ↔ ∀ i ∈ s, f i ≤ g i :=
  ⟨fun h s _hs => h s, fun h s => by
    classical exact if H : s ∈ f.support then h s (hf H) else (notMem_support_iff.1 H).symm ▸ zero_le (g s)⟩

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