verticalStrip — Mathlib

English

Definition: verticalStrip(A,B) is the set of z ∈ ℍ with |Re z| ≤ A and Im z ≥ B.

Русский

Определение: verticalStrip(A,B) — множество z ∈ ℍ с |Re z| ≤ A и Im z ≥ B.

LaTeX

$$$verticalStrip(A,B) = \\{ z ∈ \\mathbb{H} : |\\\\operatorname{Re}(z)| \\\\le A \\\\land \\\\operatorname{Im}(z) \\\\ge B \\}$.$$

Lean4

/-- The vertical strip of width `A` and height `B`, defined by elements whose real part has absolute
value less than or equal to `A` and imaginary part is at least `B`. -/
def verticalStrip (A B : ℝ) :=
  {z : ℍ | |z.re| ≤ A ∧ B ≤ z.im}

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