closure_halfSpace — Mathlib

English

The frontier of the half-space { y | a ≤ y_i } is the boundary { a = y_i }.

Русский

Граница полупространства { y | a ≤ y_i } состоит из точек с равенством a = y_i.

LaTeX

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

Lean4

@[simp]
theorem closure_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 ⁻¹' Ici a) = f ⁻¹' Ici a
  rw [f.closure_preimage, closure_Ici]
  apply Function.surjective_eval

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