English
In the Euclidean quadrant, the interior of { y : ∀ i, a ≤ y_i } equals { y : ∀ i, a < y_i }.
Русский
В Евклидовой четверти interior множества { y : для всех i, a ≤ y_i } равно { y : для всех i, a < y_i }.
LaTeX
$$$\\mathrm{int}\\{ y : \\forall i, a \\le y_i \\} = \\{ y : \\forall i, a < y_i \\}$$$
Lean4
theorem interior_euclideanQuadrant (n : ℕ) (p : ℝ≥0∞) (a : ℝ) :
interior {y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a ≤ y i} = {y | ∀ i : Fin n, a < y i} :=
by
let f : Fin n → StrongDual ℝ (Π _ : Fin n, ℝ) := fun i ↦ ContinuousLinearMap.proj i
have h : {y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a ≤ y i} = ⋂ i, (f i) ⁻¹' Ici a := by ext; simp; rfl
have h' : {y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a < y i} = ⋂ i, (f i) ⁻¹' Ioi a := by ext; simp; rfl
rw [h, h', interior_iInter_of_finite]
apply iInter_congr fun i ↦ ?_
rw [(f i).interior_preimage, interior_Ici]
apply Function.surjective_eval
