English
Let a ∈ ℝ and b1 ≤ b2 with b1,b2 ∈ ℝ. The vertical segment [b1,b2] translated by a is the complex line segment { a + i y : y ∈ [b1,b2] }, i.e., { z ∈ ℂ : Re z = a and Im z ∈ [b1,b2] }.
Русский
Пусть a ∈ ℝ и b1 ≤ b2. Вертикальный отрезок [b1,b2], сдвинутый на a, представляет собой комплексную линейную диагональ: { a + i y : y ∈ [b1,b2] }, то есть { z ∈ ℂ : Re z = a и Im z ∈ [b1,b2] }.
LaTeX
$$$$ \{ a + i y : y \in [b_1, b_2] \} = \{ z \in \mathbb{C} : \Re z = a \wedge \Im z \in [b_1, b_2] \} $$$$
Lean4
/-- A vertical segment `[b₁, b₂]` translated by `a` is the complex line segment. -/
theorem verticalSegment_eq (a b₁ b₂ : ℝ) : (fun (y : ℝ) ↦ a + y * I) '' [[b₁, b₂]] = { a } ×ℂ [[b₁, 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
simp only [equivRealProd_apply, singleton_prod, mem_image, Prod.mk.injEq, exists_eq_right_right, mem_preimage] at hx
obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
refine ⟨x.im, x₁, by simp⟩
