interpStrip_scale — Mathlib

English

For any f and l<u, interpStrip (scale f l u) ((z - l)/(u - l)) equals interpStrip' f l u z.

Русский

Для любого f и l<u, interpStrip (scale f l u) ((z - l)/(u - l)) равно interpStrip' f l u z.

LaTeX

$$$\\displaystyle \\interpStrip\\,(\\text{scale } f\\, l\\, u)\\,\\frac{z - l}{u - l} = \\interpStrip'\\, f\\, l\\, u\\, z.$$$

Lean4

/-- A technical lemma relating the bounds given by the three lines lemma on a general strip
to the bounds for its scaled version on the strip ``re ⁻¹' [0, 1]`. -/
theorem interpStrip_scale (f : ℂ → E) {l u : ℝ} (hul : l < u) (z : ℂ) :
    interpStrip (scale f l u) ((z - ↑l) / (↑u - ↑l)) = interpStrip' f l u z :=
  by
  simp only [interpStrip, interpStrip']
  simp_rw [sSupNormIm_scale_left f hul, sSupNormIm_scale_right f hul]

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