mem_verticalStrip_iff

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.mem_verticalStrip_iff

English

Membership in verticalStrip is equivalent to |Re z| ≤ A and Bi z ≥ B.

Русский

Членство в verticalStrip эквивалентно |Re z| ≤ A и Im z ≥ B.

LaTeX

$$z ∈ verticalStrip(A,B) iff |Re(z)| ≤ A ∧ B ≤ Im(z).$$

Lean4

theorem mem_verticalStrip_iff (A B : ℝ) (z : ℍ) : z ∈ verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im :=
  Iff.rfl

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

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

Разделы

Аффилиация

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