English
Let a1 ≤ a2 and b ∈ ℝ. The real segment [a1, a2] translated by b i is the complex line segment consisting of all points x + i b with x ∈ [a1, a2], i.e. the set [a1,a2] × {b}.
Русский
Пусть a1 ≤ a2 и b ∈ ℝ. Реальный отрезок [a1, a2], сдвинутый на b i, образует комплексную линейную диагональ: { x + i b : x ∈ [a1,a2] } = [a1, a2] × { b }.
LaTeX
$$$$ \{ x + i b : x \in [a_1, a_2] \} = \{ z \in \mathbb{C} : \Re z \in [a_1, a_2] \wedge \Im z = b \} $$$$
Lean4
/-- A real segment `[a₁, a₂]` translated by `b * I` is the complex line segment. -/
theorem horizontalSegment_eq (a₁ a₂ b : ℝ) : (fun (x : ℝ) ↦ x + b * I) '' [[a₁, a₂]] = [[a₁, a₂]] ×ℂ { b } :=
by
rw [← preimage_equivRealProd_prod]
ext x
constructor
· intro hx
obtain ⟨x₁, hx₁, hx₁'⟩ := hx
simp [← hx₁', mem_preimage, mem_prod, hx₁]
· intro hx
obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
refine ⟨x.re, x₁, by simp⟩
