closure_setOf_re_lt — Mathlib

English

The closure of the set {z ∈ ℂ | z.re < a} is the set {z ∈ ℂ | z.re ≤ a}.

Русский

Замыкание множества {z ∈ ℂ | z.re < a} равно {z ∈ ℂ | z.re ≤ a}.

LaTeX

$$$\mathrm{closure}\{z\in\mathbb{C} : z_{\mathrm{re}} < a\} = \{z\in\mathbb{C} : z_{\mathrm{re}} \le a\}$$$

Lean4

@[simp]
theorem closure_setOf_re_lt (a : ℝ) : closure {z : ℂ | z.re < a} = {z | z.re ≤ a} := by
  simpa only [closure_Iio] using closure_preimage_re (Iio a)

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