card_support_eq_one — Mathlib

English

For f ∈ α →₀ M, the cardinality of its support is 1 iff there exists a with f(a) ≠ 0 and f = single a (f(a)).

Русский

Для f ∈ α →₀ M кардинальность опоры равна 1 тогда и только тогда, когда существует a such that f(a) ≠ 0 и f = single a (f(a)).

LaTeX

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

Lean4

theorem card_support_eq_one {f : α →₀ M} : #f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a) := by
  simp only [card_eq_one, support_eq_singleton]

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