scale_id_mem_verticalStrip_of_mem_verticalStrip

English

Scaling by l,u maps the closed vertical strip to the corresponding one; this transformation preserves membership structure under a simple affine map.

Русский

Масштабирование переводит закрытую вертикальную полосу в соответствующую, сохраняя принадлежность через аффинное отображение.

LaTeX

$$$\\forall l

Lean4

/-- The transformation on ℂ that is used for `scale` maps the strip ``re ⁻¹' (l, u)``
  to the strip ``re ⁻¹' (0, 1)``. -/
theorem scale_id_mem_verticalStrip_of_mem_verticalStrip {l u : ℝ} (hul : l < u) {z : ℂ} (hz : z ∈ verticalStrip 0 1) :
    l + z * (u - l) ∈ verticalStrip l u :=
  by
  simp only [verticalStrip, mem_preimage, mem_Ioo] at hz
  simp only [verticalStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im, ofReal_im, sub_self, mul_zero,
    sub_zero, mem_Ioo, lt_add_iff_pos_right]
  obtain ⟨hz₁, hz₂⟩ := hz
  simp only [hz₁, mul_pos_iff_of_pos_left, sub_pos, hul, true_and]
  rw [add_comm, ← sub_lt_sub_iff_right l, add_sub_assoc, sub_self, add_zero]
  nth_rewrite 2 [← one_mul (u - l)]
  gcongr
  simp only [sub_pos]
  exact hul

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