lean_workbook_plus_26104
ProvedProve that among any real numbers there exist two, say and , such that: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_26104 (A : Finset ℝ) (hA : A.card >= 7) :
∃ x y : ℝ, x ∈ A ∧ y ∈ A ∧ (0 : ℝ) ≤ (x - y) / (1 + x * y) ∧
(x - y) / (1 + x * y) ≤ 1 / Real.sqrt 3 := by sorrySource