frontier_setOf_im_le — 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_im_le (a : ℝ) : frontier {z : ℂ | z.im ≤ a} = {z | z.im = a} := by
  simpa only [frontier_Iic] using frontier_preimage_im (Iic a)

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