frontier_halfSpace — Mathlib

English

The range of the inclusion from Euclidean Quadrant n is exactly the set of vectors with all coordinates nonnegative.

Русский

Образ включения из Евклидовой четверти n равен множеству векторов с неотрицательными координатами.

LaTeX

$$$\\mathrm{range}(\\mathrm{Subtype}.val : \\mathrm{EuclideanQuadrant}(n) \\to \\Pi_{i:\\mathrm{Fin}(n)} \\mathbb{R}) = \\{ y : \\forall i: \\mathrm{Fin}(n), \\; 0 \\le y(i) \\}$$$

Lean4

@[simp]
theorem frontier_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
    frontier {y : PiLp p (fun _ : Fin n ↦ ℝ) | a ≤ y i} = {y | a = y i} :=
  by
  rw [frontier, closure_halfSpace, interior_halfSpace]
  ext y
  simpa only [mem_diff, mem_setOf_eq, not_lt] using antisymm_iff

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