falling — Mathlib

English

For a family of sets 𝒜, if 𝒜 is intersecting, then the falling operation preserves existence of common elements when taking shadows.

Русский

Для семейства множеств 𝒜, если 𝒜 пересекающееся, то операция падения сохраняет существование общего элемента в тенях.

LaTeX

$$$\forall s, t \; (s,t \in 𝒜) \Rightarrow ∃ a \in s \cap t$$$

Lean4

/-- `falling k 𝒜` is all the finsets of cardinality `k` which are a subset of something in `𝒜`. -/
def falling : Finset (Finset α) :=
  𝒜.sup <| powersetCard k

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