verticalClosedStrip — Mathlib

English

The closed vertical strip through a and b is the set { z ∈ C : Re z ∈ [a,b] }.

Русский

Закрытая вертикальная полоса через a и b — множество { z ∈ ℂ : Re z ∈ [a,b] }.

LaTeX

$$$\mathrm{verticalStripClosed}(a,b) = \{ z \in \mathbb{C} : \Re z \in [a,b] \}$$$

Lean4

/-- The vertical strip in the complex plane containing all `z ∈ ℂ` such that `z.re ∈ Icc a b`. -/
def verticalClosedStrip (a : ℝ) (b : ℝ) : Set ℂ :=
  re ⁻¹' Icc a b

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