Skip to content

Erdős problem 701

Let F\mathcal{F} be a family of sets closed under taking subsets (i.e. if B⊆A∈FB\subseteq A\in\mathcal{F} then B∈FB\in \mathcal{F}). There exists some element xx such that whenever F′⊆F\mathcal{F}'\subseteq \mathcal{F} is an intersecting subfamily we have ∣F′∣≤∣{A∈F:x∈A}∣.\lvert \mathcal{F}'\rvert \leq \lvert \{ A\in \mathcal{F} : x\in A\}\rvert.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/701.lean

Formal Conjectures

FormalConjectures/ErdosProblems/701.leanErdos701.erdos_7013 linesExact file
True ↔  ∀ {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

Continue