isOpen_slitPlane — Mathlib

English

The slit plane, defined as C minus the non-positive real axis (-∞,0], is an open subset of the complex plane. Equivalently, it can be described as the union of the right half-plane {Re z > 0} and the set {Im z ≠ 0}.

Русский

Слитная плоскость, равная C \ (-∞,0], является открытым подмножеством комплексной плоскости. В частности, её можно записать как объединение {Re z > 0} и {Im z ≠ 0}.

LaTeX

$$$\\mathrm{IsOpen}(\\text{slitPlane})$$$

Lean4

theorem isOpen_slitPlane : IsOpen slitPlane :=
  (isOpen_lt continuous_const continuous_re).union (isOpen_ne_fun continuous_im continuous_const)

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