shatters_empty — Mathlib

English

For any α and any finite family 𝒜 of finite subsets of α, 𝒜 shatters the empty set ∅ if and only if 𝒜 is nonempty.

Русский

Для любого α и любого конечного семейства 𝒜 конечных подмножеств α выполняется, что 𝒜 шаттерит пустое множество тогда и только тогда, когда 𝒜 непусто.

LaTeX

$$$\\mathcal{A}.Shatters\\emptyset \\leftrightarrow \\mathcal{A}.Nonempty$$$

Lean4

@[simp]
theorem shatters_empty : 𝒜.Shatters ∅ ↔ 𝒜.Nonempty :=
  ⟨Shatters.nonempty, fun ⟨s, hs⟩ t ht ↦ ⟨s, hs, by rwa [empty_inter, eq_comm, ← subset_empty]⟩⟩

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