length_Ioc — Mathlib

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₂))

Похожие утверждения