card_eq_succ_iff_cons — Mathlib

English

A Finset s has cardinality n+1 iff there exist an element a and a Finset t with a not in t such that s = cons a t and |t| = n.

Русский

Кардиналитет Finset s равен n+1 тогда и только тогда, существует элемент a и подмножество t с a не принадлежит t, такое что s = cons a t и |t| = n.

LaTeX

$$$#s = n + 1 \\iff \\exists a t, a \\notin t ∧ cons a t a = s ∧ #t = n$$$

Lean4

theorem card_eq_succ_iff_cons : #s = n + 1 ↔ ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n :=
  ⟨cons_induction_on s (by simp) fun a s _ _ _ => ⟨a, s, by simp_all⟩, fun ⟨a, t, _, hs, _⟩ => by simpa [← hs]⟩

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