falling_zero_subset — Mathlib

English

If we remove zero elements (the 0-th shadow) from every member of a finite family 𝒜 of finite sets, all resulting sets are empty. In other words, falling 0 𝒜 ⊆ {∅}.

Русский

Если удалить нулевые элементы (нулевую тень) из каждого множества в конечном семействе 𝒜 конечных множеств, получаются только пустые множества; то есть falling 0 𝒜 ⊆ {∅}.

LaTeX

$$$$ \\mathrm{falling}_0(𝒜) \\subseteq \\{ \\emptyset \\} $$$$

Lean4

theorem falling_zero_subset : falling 0 𝒜 ⊆ {∅} :=
  subset_singleton_iff'.2 fun _ ht => card_eq_zero.1 <| sized_falling _ _ ht

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