existsUnique_iff_card_one — Mathlib

English

There exists a unique a with p(a) if and only if the set {x | p(x)} has cardinality 1.

Русский

Существует ровно один элемент a с свойством p(a) тогда и только тогда множество {x | p(x)} имеет кардинальность 1.

LaTeX

$$$(\exists! a:\alpha, p(a)) \iff |\{x:\alpha \mid p(x)\}| = 1$$$

Lean4

theorem existsUnique_iff_card_one {α} [Fintype α] (p : α → Prop) [DecidablePred p] : (∃! a : α, p a) ↔ #{x | p x} = 1 :=
  by
  rw [Finset.card_eq_one]
  refine exists_congr fun x => ?_
  simp only [Subset.antisymm_iff, subset_singleton_iff', singleton_subset_iff, and_comm, mem_filter_univ]

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