ncard_le_one_of_subsingleton — Mathlib

English

If α is a Subsingleton, then any subset s has cardinality at most 1: s.ncard ≤ 1.

Русский

Если α является подсинглотоном, то каждый подмножество s имеет кардинальность не более 1: s.ncard ≤ 1.

LaTeX

$$$$ [\text{Subsingleton } \alpha] \; s.ncard \le 1 $$$$

Lean4

/-- A `Set` of a subsingleton type has cardinality at most one. -/
theorem ncard_le_one_of_subsingleton [Subsingleton α] (s : Set α) : s.ncard ≤ 1 :=
  by
  rw [ncard_eq_toFinset_card]
  exact Finset.card_le_one_of_subsingleton _

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