card_eq_four — Mathlib

English

Let s be a multiset. Then |s| = 4 if and only if there exist x, y, z, w with s = {x, y, z, w}.

Русский

Пусть s — мультисет. Тогда |s| = 4 тогда и только тогда, когда существуют элементы x, y, z, w такие, что s = {x, y, z, w}.

LaTeX

$$$|s| = 4 \iff \exists x,y,z,w,\ s = \{ x, y, z, w \}$$$

Lean4

theorem card_eq_four {s : Multiset α} : card s = 4 ↔ ∃ x y z w, s = { x, y, z, w } :=
  ⟨Quot.inductionOn s fun _l h =>
      (List.length_eq_four.mp h).imp fun _a =>
        Exists.imp fun _b => Exists.imp fun _c => Exists.imp fun _d => congr_arg _,
    fun ⟨_a, _b, _c, _d, e⟩ => e.symm ▸ rfl⟩

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