English
The scaled map preserves vertical closed strip membership via a simple affine transform.
Русский
Скалированная карта сохраняет принадлежность закрытой вертикальной полосе через простое аффинное преобразование.
LaTeX
$$$\\forall z \\in \\text{verticalClosedStrip } l u,\\; z/(u-l) - l/(u-l) \\in \\text{verticalClosedStrip } 0 1.$$$
Lean4
/-- The function `scale f l u` is `diffContOnCl`. -/
theorem scale_diffContOnCl {f : ℂ → E} {l u : ℝ} (hul : l < u) (hd : DiffContOnCl ℂ f (verticalStrip l u)) :
DiffContOnCl ℂ (scale f l u) (verticalStrip 0 1) :=
by
unfold scale
apply DiffContOnCl.comp (s := verticalStrip l u) hd
· apply DiffContOnCl.const_add
apply DiffContOnCl.smul_const
exact Differentiable.diffContOnCl differentiable_id
· rw [MapsTo]
intro z hz
exact scale_id_mem_verticalStrip_of_mem_verticalStrip hul hz
