lemma
proved
tactic proof
Jcost_continuous_pos
show as:
view Lean formalization →
formal statement (Lean)
130lemma Jcost_continuous_pos : ContinuousOn Jcost (Ioi 0) := by
proof body
Tactic-mode proof.
131 classical
132 have h1 : ContinuousOn (fun x : ℝ => x) (Ioi 0) := continuousOn_id
133 have h2 : ContinuousOn (fun x : ℝ => x⁻¹) (Ioi 0) := by
134 refine ContinuousOn.inv₀ (f:=fun x : ℝ => x) (s:=Ioi 0) h1 ?hneq
135 intro x hx; exact ne_of_gt hx
136 have h3 : ContinuousOn (fun x : ℝ => x + x⁻¹) (Ioi 0) := h1.add h2
137 have h4 : ContinuousOn (fun x : ℝ => (1 / 2 : ℝ) * (x + x⁻¹)) (Ioi 0) :=
138 (continuousOn_const).mul h3
139 have h5 : ContinuousOn (fun x : ℝ => (1 / 2 : ℝ) * (x + x⁻¹) - 1) (Ioi 0) :=
140 h4.sub continuousOn_const
141 simpa [Jcost, one_div, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc, sub_eq_add_neg]
142 using h5
143
144/-- `Jcost` satisfies reciprocal symmetry in the theorem-surface format. -/