frontier_setOf_le_im — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem frontier_setOf_le_im (a : ℝ) : frontier {z : ℂ | a ≤ z.im} = {z | z.im = a} := by
  simpa only [frontier_Ici] using frontier_preimage_im (Ici a)

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