closure_open_halfSpace — Mathlib

English

The interior of a half-space { y | a ≤ y_i } equals { y | a < y_i }.

Русский

interior полупространства { y | a ≤ y_i } равен { y | a < y_i }.

LaTeX

$$$\\operatorname{interior}\\{ y : a \\le y_i \\} = \\{ y : a < y_i \\}$$$

Lean4

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

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