interior_setOf_le_re — Mathlib

English

Let a be a real number. Then the interior of the set { z ∈ ℂ : Re z ≥ a } is { z ∈ ℂ : Re z > a }.

Русский

Пусть a ∈ ℝ. Тогда interior множества { z ∈ ℂ : Re z ≥ a } совпадает с { z ∈ ℂ : Re z > a }.

LaTeX

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

Lean4

@[simp]
theorem interior_setOf_le_re (a : ℝ) : interior {z : ℂ | a ≤ z.re} = {z | a < z.re} := by
  simpa only [interior_Ici] using interior_preimage_re (Ici a)

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