support_eq_singleton' — Mathlib

English

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

Русский

Для любых f и a верно: опора f равна {a} тогда и только тогда, когда существует b ≠ 0, что f = single a b.

LaTeX

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

Lean4

theorem support_eq_singleton' {f : α →₀ M} {a : α} : f.support = { a } ↔ ∃ b ≠ 0, f = single a b :=
  ⟨fun h =>
    let h := support_eq_singleton.1 h
    ⟨_, h.1, h.2⟩,
    fun ⟨_b, hb, hf⟩ => hf.symm ▸ support_single_ne_zero _ hb⟩

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