interior_setOf_le_im — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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