card_eq_one — Mathlib

English

The statement card_eq_two gives a structural description of when a multiset has cardinality 2.

Русский

Утверждение card_eq_two даёт структурное описание того, когда кардинал мультимножества равен 2.

LaTeX

$$card s = 2 \iff \exists x y, s = {x, y}$$

Lean4

theorem card_eq_one {s : Multiset α} : card s = 1 ↔ ∃ a, s = { a } :=
  ⟨Quot.inductionOn s fun _l h => (List.length_eq_one_iff.1 h).imp fun _a => congr_arg _, fun ⟨_a, e⟩ => e.symm ▸ rfl⟩

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