Let $X$ be a set of cardinality $\aleph_\omega$ and $f$ be a function from the finite subsets of
$X$ to $X$ such that $f(A)\not\in A$ for all $A$. Must there exist an infinite $Y\subseteq X$
that is independent - that is, for all finite $B\subset Y$ we have $f(B)\not\in Y$?
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_623 : answer(sorry) ↔ ∀ (X : Type u) (hX : #X = ℵ_ ω)
(f : Finset X → X), (∀ A : Finset X, f A ∉ A) →
(∃ Y : Set X, Set.Infinite Y ∧ (∀ (B : Finset X), ↑B ⊆ Y → f B ∉ Y))
