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.

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

701.lean

Retained formal statement1 of 1

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.

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

Search problems.science

Find a Problem, Result, source, or page