support_subset_singleton' — Mathlib

English

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

Русский

Для любого f и a: f.support ⊆ {a} тогда и только тогда, когда существует b, f = single a b.

LaTeX

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

Lean4

theorem support_subset_singleton' {f : α →₀ M} {a : α} : f.support ⊆ { a } ↔ ∃ b, f = single a b :=
  ⟨fun h => ⟨f a, support_subset_singleton.mp h⟩, fun ⟨b, hb⟩ => by rw [hb, support_subset_singleton, single_eq_same]⟩

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