Affine bijections of horizontal strips

Positive real scalings and complex translations map horizontal strips bijectively onto the strips whose endpoints undergo the corresponding real affine map. These maps rescale logarithmic strip coordinates to arbitrary boundary heights.

theorem TauCeti.bijOn_ofReal_mul_add_horizontalStrip {s : ℝ} (hs : 0 < s) (c : ℂ) (l h : ℝ) : Set.BijOn (fun (w : ℂ) => ↑s * w + c) {w : ℂ | w.im ∈ Set.Ioo l h} {w : ℂ | w.im ∈ Set.Ioo (s * l + c.im) (s * h + c.im)}

A positive real scaling followed by a complex translation maps a horizontal strip bijectively onto the strip with the transformed imaginary endpoints.