toFinset_card_eq_one_iff — Mathlib

English

The toFinset cardinality is 1 exactly when s has nonzero cardinality and is a multiple of a singleton.

Русский

card toFinset равно 1 тогда и только тогда, когда s имеет ненулевую кардинальность и равна кардинальности s как кратному одному элементу множества.

LaTeX

$$$#(s.toFinset) = 1 \iff \operatorname{card}(s) \neq 0 \land \exists a:\alpha, s = \operatorname{card}(s) \cdot \{a\}$$$

Lean4

theorem toFinset_card_eq_one_iff (s : Multiset α) :
    #s.toFinset = 1 ↔ Multiset.card s ≠ 0 ∧ ∃ a : α, s = Multiset.card s • { a } := by
  simp_rw [Finset.card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]

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