card_eq_two — Mathlib

English

Alternate formulation: card s = 2 iff there exist x,y with s = {x,y}.

Русский

Альтернативная формулировка: card s = 2 тогда и только тогда, когда существуют x,y такие что s = {x,y}.

LaTeX

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

Lean4

theorem card_eq_two {s : Multiset α} : card s = 2 ↔ ∃ x y, s = { x, y } :=
  ⟨Quot.inductionOn s fun _l h => (List.length_eq_two.mp h).imp fun _a => Exists.imp fun _b => congr_arg _,
    fun ⟨_a, _b, e⟩ => e.symm ▸ rfl⟩

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