Interior, closure of half space

Stream: Is there code for X?

[Michael Rothgang]

I am sure these exist somewhere, also more generally (probably, for general L^p spaces over $\mathbb{R}$), but am not quite sure where to look. Can a better expert give me a pointer?

theorem interior_halfspace {a : ℝ} (n : ℕ) [Zero (Fin n)] :
    interior {y : EuclideanSpace ℝ (Fin n)| a ≤ y 0} = {y | a < y 0} := by
  sorry

lemma isClosed_halfspace {a : ℝ} (n : ℕ) [Zero (Fin n)] :
    IsClosed {y : EuclideanSpace ℝ (Fin n) | a ≤ y 0} := sorry

[Yaël Dillies]

Can you get this down to the one dimensional case somehow?

[Eric Wieser]

You could take the image of lineMap

[Eric Wieser]

theorem interior_halfspace {a : ℝ} (n : ℕ) [NeZero n] :
    interior {y : EuclideanSpace ℝ (Fin n) | a ≤ y 0} = {y | a < y 0} := by
  let f : (EuclideanSpace ℝ (Fin n)) →L[ℝ] ℝ := ContinuousLinearMap.proj 0
  change interior (f ⁻¹' Set.Ici a) = f ⁻¹' Set.Ioi a
  rw [f.interior_preimage (Function.surjective_eval _), interior_Ici]

[Michael Rothgang]

I was slowly on my way towards working this out, and you just solved this. Really nice, thank you!

[Eric Wieser]

I suppose adding lemma like this for common surjective continuous linear maps is reasonable? I think we already have the Complex.re version

[Michael Rothgang]

#15890 adds these lemmas, and a few related ones. Comments welcome.