support_subset_singleton — Mathlib

English

For f ∈ α →₀ M and a ∈ α, f.support ⊆ {a} if and only if f = single a (f(a)).

Русский

Для любой f и a: f.support ⊆ {a} тогда и только тогда, когда f = single a (f(a)).

LaTeX

$$$f.\operatorname{support} \subseteq \{a\} \iff f = \mathrm{single}(a,f(a))$$$

Lean4

theorem support_subset_singleton {f : α →₀ M} {a : α} : f.support ⊆ { a } ↔ f = single a (f a) :=
  ⟨fun h => eq_single_iff.mpr ⟨h, rfl⟩, fun h => (eq_single_iff.mp h).left⟩

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