card_support_eq_one' — Mathlib

English

For f ∈ α →₀ M, the card of its support equals 1 iff ∃ a ∈ α, ∃ b ≠ 0 with f = single a b.

Русский

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

LaTeX

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

Lean4

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

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