subsingleton' — Mathlib

English

If α is finite and A is a set of Finsets of α with size card α, then A has at most one element.

Русский

Если α конечен и A — множество Finset α с размером, равным кардиналу α, то A содержит не более одного элемента.

LaTeX

$$$[Fintype\\;\\alpha] \\quad A.Sized(|\\alpha|) \\Rightarrow A\\text{ 是 subsingleton }\\; (|A| \\le 1).$$$

Lean4

theorem subsingleton' [Fintype α] (hA : A.Sized (Fintype.card α)) : A.Subsingleton :=
  subsingleton_of_forall_eq Finset.univ fun s hs => s.card_eq_iff_eq_univ.1 <| hA hs

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