card_eq_three — Mathlib

English

The cardinality equals three iff there exist x, y, z with s = {x, y, z}.

Русский

Кардинал равен трём тогда и только тогда, когда существуют x, y, z такие, что s = {x, y, z}.

LaTeX

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

Lean4

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

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