Erdős problem 701
Let be a family of sets closed under taking subsets (i.e. if then ). There exists some element such that whenever is an intersecting subfamily we have
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/701.leanTrue ↔ ∀ {X : Type} [Nonempty X] [Fintype X] (F : Set (Set X)), IsLowerSet F → ∃ x, ∀ F' ⊆ F, F'.Intersecting → Cardinal.mk ↑F' ≤ Cardinal.mk ↑{A | A ∈ F ∧ x ∈ A}OpenStatement only, no proof