compl_Iic_zero

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.compl_Iic_zero

English

The complement of the set {z ∈ ℂ : z ≤ 0} is exactly the slit plane.

Русский

Дополнение множества {z ∈ ℂ : z ≤ 0} совпадает с слитной плоскостью.

LaTeX

$$\\big( \\{ z \\in \\mathbb{C} : z \\le 0 \\} \\big)^{c} = \\text{slitPlane}$$

Lean4

protected theorem compl_Iic_zero : (Set.Iic 0)ᶜ = slitPlane :=
  Set.ext fun _ ↦ mem_slitPlane_iff_not_le_zero.symm

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

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

Разделы

Аффилиация

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