support_eq_singleton — Mathlib

English

For f ∈ α →₀ M, f.support = {a} iff f(a) ≠ 0 and f = single a (f(a)).

Русский

Для f ∈ α →₀ M опора f равна {a} тогда и только тогда, когда f(a) ≠ 0 и f = single a (f(a)).

LaTeX

$$$\operatorname{supp}(f) = \{a\} \iff f(a) \neq 0 \wedge f = \mathrm{single}(a,f(a))$$$

Lean4

theorem support_eq_singleton {f : α →₀ M} {a : α} : f.support = { a } ↔ f a ≠ 0 ∧ f = single a (f a) :=
  ⟨fun h => ⟨mem_support_iff.1 <| h.symm ▸ Finset.mem_singleton_self a, eq_single_iff.2 ⟨subset_of_eq h, rfl⟩⟩, fun h =>
    h.2.symm ▸ support_single_ne_zero _ h.1⟩

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