English
The image of the closed vertical strip under scaling lies in the corresponding vertical closed strip after an affine change of variable.
Русский
Образ закрытой вертикальной полосы при масштабировании принадлежит соответствующей закрытой полосе после аффинного переноса переменных.
LaTeX
$$$\\text{If } z \\in \\text{verticalClosedStrip } 0 1,\\; l + z(u-l) \\in \\text{verticalClosedStrip } l u.$$$
Lean4
/-- The transformation on ℂ that is used for `scale` maps the closed strip ``re ⁻¹' [l, u]``
to the closed strip ``re ⁻¹' [0, 1]``. -/
theorem scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip {l u : ℝ} (hul : l < u) {z : ℂ}
(hz : z ∈ verticalClosedStrip 0 1) : l + z * (u - l) ∈ verticalClosedStrip l u :=
by
simp only [verticalClosedStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im, ofReal_im, sub_self,
mul_zero, sub_zero, mem_Icc, le_add_iff_nonneg_right]
simp only [verticalClosedStrip, mem_preimage, mem_Icc] at hz
obtain ⟨hz₁, hz₂⟩ := hz
simp only [sub_pos, hul, mul_nonneg_iff_of_pos_right, hz₁, true_and]
rw [add_comm, ← sub_le_sub_iff_right l, add_sub_assoc, sub_self, add_zero]
nth_rewrite 2 [← one_mul (u - l)]
have := sub_nonneg.2 hul.le
gcongr
