verticalStrip

Mathlib.Analysis.Complex.Hadamard

URI: https://scilib.ai/kg/mathlib#Complex.HadamardThreeLines.verticalStrip

← MathLib Explorer

English

The vertical strip through a and b is the set { z ∈ C : Re z ∈ (a,b) }.

Русский

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

LaTeX

$$$\mathrm{verticalStrip}(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 ∈ Ioo a b`. -/
def verticalStrip (a : ℝ) (b : ℝ) : Set ℂ :=
  re ⁻¹' Ioo a b

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru