199.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/199
[Ba75] Baumgartner, James E., Partitioning vector spaces. J. Combinatorial Theory Ser. A (1975), 231-233.

Imports (1)

theorem Erdos199.erdos_199 sorry line 40 source
depends on sorry what this means
Statement uses: Iff, False, Set, Real, ThreeAPFree, Exists, And, Set.IsAPOfLength, Top.top, ENat, LE.le, Compl.compl
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
11 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.