Skip to content

Erdős problem 701

Start work

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

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

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