nonempty — Mathlib

English

Let α be a type and 𝒜 a finite family of finite subsets of α. If 𝒜 shatters a finite set s, then 𝒜 is nonempty.

Русский

Пусть α — множество с конечной размерностью; 𝒜 — конечное семейство конечных подмножеств α. Если 𝒜 разворачивает (шаттерирует) множество s, то 𝒜 не пусто.

LaTeX

$$$\\mathcal{A}\\text{ Shatters } s \\Rightarrow \\mathcal{A} \\neq \\emptyset$$$

Lean4

protected theorem nonempty (h : 𝒜.Shatters s) : 𝒜.Nonempty :=
  let ⟨t, ht, _⟩ := h Subset.rfl;
  ⟨t, ht⟩

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