subsingleton — Mathlib

English

If A is a family of Finset α with size r = 0, then A is subsingleton; i.e., any two members of A are equal.

Русский

Если A состоит из финсет α размером 0, то A — подсингултон; то есть любые два элемента A равны.

LaTeX

$$$ A.Sized 0 \Rightarrow A.Subsingleton $$$

Lean4

protected theorem subsingleton (hA : A.Sized 0) : A.Subsingleton :=
  subsingleton_of_forall_eq ∅ fun _s hs => card_eq_zero.1 <| hA hs

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