Skip to content

Erdős problem 701

Let F\mathcal{F} be a family of sets closed under taking subsets (i.e. if BAFB\subseteq A\in\mathcal{F} then BFB\in \mathcal{F}). There exists some element xx such that whenever FF\mathcal{F}'\subseteq \mathcal{F} is an intersecting subfamily we have F{AF:xA}.\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'.IntersectingCardinal.mkF'Cardinal.mk ↑{A | AFxA}
OpenStatement only, no proof

Continue

Search problems.science

Find a Problem, Result, source, or page