frontier_setOf_lt_re — 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 < \\operatorname{Re} z \\}) = \\{ z \\in \\mathbb{C} : \\operatorname{Re} z = a \\}$$$

Lean4

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

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