theorem
proved
tactic proof
nothing_cannot_exist
show as:
view Lean formalization →
formal statement (Lean)
130theorem nothing_cannot_exist (C : ℝ) :
131 ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x := by
proof body
Tactic-mode proof.
132 -- Choose ε = 1/(2(|C|+2)) so that 1/x > 2(|C|+2) when x < ε
133 use 1 / (2 * (|C| + 2))
134 constructor
135 · positivity
136 · intro x hxpos hxlt
137 -- x < 1/(2(|C|+2)) implies 1/x > 2(|C|+2)
138 have hbound : 0 < 2 * (|C| + 2) := by positivity
139 have hinv : 2 * (|C| + 2) < x⁻¹ := by
140 rw [inv_eq_one_div, lt_one_div hbound hxpos]
141 exact hxlt
142 simp only [defect, J]
143 have hxinv_pos : 0 < x⁻¹ := inv_pos.mpr hxpos
144 -- (x + 1/x)/2 - 1 ≥ 1/x / 2 - 1 > (2(|C|+2))/2 - 1 = |C| + 1 ≥ C + 1 > C
145 have h1 : x⁻¹ / 2 > |C| + 1 := by linarith
146 have h2 : (x + x⁻¹) / 2 ≥ x⁻¹ / 2 := by
147 have : x ≥ 0 := le_of_lt hxpos
148 linarith
149 have h3 : |C| ≥ C := le_abs_self C
150 linarith
151
152/-! ## Structured Set -/
153
154/-- The structured set S = {x ∈ ℝ₊ : defect(x) = 0} = {1}. -/