English
The length of the interval Ioc(a,b) equals f(b)−f(a) in real-terms.
Русский
Длина интервала Ioc(a,b) равна f(b)−f(a).
LaTeX
$$$$ f.length(Ioc(a,b)) = \\mathrm{ofReal}(f(b) - f(a)). $$$$
Lean4
@[simp]
theorem length_Ioc (a b : ℝ) : f.length (Ioc a b) = ofReal (f b - f a) :=
by
refine
le_antisymm (iInf_le_of_le a <| iInf₂_le b Subset.rfl)
(le_iInf fun a' => le_iInf fun b' => le_iInf fun h => ENNReal.coe_le_coe.2 ?_)
rcases le_or_gt b a with ab | ab
· rw [Real.toNNReal_of_nonpos (sub_nonpos.2 (f.mono ab))]
apply zero_le
obtain ⟨h₁, h₂⟩ := (Ioc_subset_Ioc_iff ab).1 h
exact Real.toNNReal_le_toNNReal (sub_le_sub (f.mono h₁) (f.mono h₂))