215.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/215
[Er83c] Erdős, Paul, Combinatorial problems in geometry. Math. Chronicle (1983), 35-54.
[JaMa02] Jackson, Steve and Mauldin, R. Daniel, Sets meeting isometric copies of the lattice $\mathbb{Z}^2$ in exactly one point. Proc. Natl. Acad. Sci. USA (2002), 15883-15887.

Imports (1)

theorem Erdos215.erdos_215 sorry line 48 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Set, Complex, Eq, Real, Norm.norm, OfNat.ofNat, ExistsUnique, And, Membership.mem, Set.image, HAdd.hAdd, HMul.hMul, Int, Complex.I
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
21 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.