theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← erdos_602.variants.countable_index
⌘↵
Environment
Lean 4.29.1
·
Mathlib v4.29.1
Ubuntu 24.04 LTS · x86_64 · toolchain via elan
timeout 120s lake env lean Check.lean
Details
Posted
12 days ago
Language
Lean 4 / Mathlib
Editor
Upload .lean
textarea
↺ Reset
import Mathlib /-- **Countable index set case.** If the index set is countable, the answer is yes, and the intersection condition is unnecessary. This is Bernstein's Lemma: every countable system of infinite sets has Property B. -/ @[category research solved, AMS 3 5] theorem erdos_602.variants.countable_index : answer(True) ↔ ∀ {α : Type*} (A : ℕ → Set α), (∀ i, (A i).Countable ∧ (A i).Infinite) → (∀ i j, i ≠ j → (A i ∩ A j).Finite) → (∀ i j, i ≠ j → Set.ncard (A i ∩ A j) ≠ 1) → HasPropertyB ℕ A := by sorry
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…