194.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/194
[ABJ11] Ardal, H. and Brown, T. and Jungić, V., Chaotic orderings of the rationals and reals. Amer. Math. Monthly (2011), 921-925.

Imports (1)

theorem Erdos194.erdos_194 sorry line 41 source
depends on sorry what this means
Statement uses: Iff, False, Nat, GE.ge, OfNat.ofNat, Real, IsStrictTotalOrder, Exists, List, And, List.IsAPOfLength, Or, List.Pairwise, flip
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.