card_support_le_one — Mathlib

English

If α is nonempty, then #f.support ≤ 1 iff ∃ a, f = single a (f a).

Русский

Если α непусто, то кардинал опоры f не превышает единицы тогда и только тогда, когда существует a, такое что f = single a (f(a)).

LaTeX

$$$#f.support \le 1 \iff \exists a, f = \mathrm{single}(a, f(a))$$$

Lean4

theorem card_support_le_one [Nonempty α] {f : α →₀ M} : #f.support ≤ 1 ↔ ∃ a, f = single a (f a) := by
  simp only [card_le_one_iff_subset_singleton, support_subset_singleton]

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