frontier_setOf_re_lt — Mathlib

English

For a real a, the frontier of { z ∈ ℂ : Re z < a } is { z ∈ ℂ : Re z = a }.

Русский

Для действительного a граница множества { z ∈ ℂ : Re z < a } равна { z ∈ ℂ : Re z = a }.

LaTeX

$$$\\operatorname{frontier}(\\{ z \\in \\mathbb{C} : \\operatorname{Re} z < a \\}) = \\{ z \\in \\mathbb{C} : \\operatorname{Re} z = a \\}$$$

Lean4

@[simp]
theorem frontier_setOf_re_lt (a : ℝ) : frontier {z : ℂ | z.re < a} = {z | z.re = a} := by
  simpa only [frontier_Iio] using frontier_preimage_re (Iio a)

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