interior_halfSpace — Mathlib

English

The closure of the closed half-space { y | a ≤ y_i } is itself.

Русский

Замыкание замкнутого полупространства равняется самому полупространству.

LaTeX

$$$\\operatorname{cl}\\{ y : a \\le y_i \\} = \\{ y : a \\le y_i \\}$$$

Lean4

@[simp]
theorem interior_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
    interior {y : PiLp p (fun _ : Fin n ↦ ℝ) | a ≤ y i} = {y | a < y i} :=
  by
  let f : StrongDual ℝ (Π _ : Fin n, ℝ) := ContinuousLinearMap.proj i
  change interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a
  rw [f.interior_preimage, interior_Ici]
  apply Function.surjective_eval

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