mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip

English

The scale map sends a point on the verticalStrip 0 1 to a point on verticalStrip l u by affine transformation.

Русский

Точка на вертикальной полосе 0 1 переходит к точке на вертикальной полосе l u по аффинному преобразованию.

LaTeX

$$$\\forall l

Lean4

/-- If z is on the closed strip `re ⁻¹' [l, u]`, then `(z - l) / (u - l)` is on the closed strip
  `re ⁻¹' [0, 1]`. -/
theorem mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip {z : ℂ} {l u : ℝ} (hul : l < u)
    (hz : z ∈ verticalClosedStrip l u) : z / (u - l) - l / (u - l) ∈ verticalClosedStrip 0 1 :=
  by
  simp only [verticalClosedStrip, Complex.div_re, mem_preimage, sub_re, mem_Icc, sub_nonneg, tsub_le_iff_right,
    ofReal_re, ofReal_im, sub_im, sub_self, mul_zero, zero_div, add_zero]
  simp only [verticalClosedStrip] at hz
  norm_cast
  simp_rw [Complex.normSq_ofReal, mul_div_assoc, div_mul_eq_div_div_swap, div_self (by linarith : u - l ≠ 0), ←
    div_eq_mul_one_div]
  constructor
  · gcongr
    · apply le_of_lt; simp [hul]
    · exact hz.1
  · rw [← sub_le_sub_iff_right (l / (u - l)), add_sub_assoc, sub_self, add_zero, div_sub_div_same,
      div_le_one (by simp [hul]), sub_le_sub_iff_right l]
    exact hz.2

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