intrinsic interior/frontier/closure

Stream: maths

[Yaël Dillies]

I'm currently defining the intrinsic interior and frontier of an arbitrary set in a LCTVS (well actually in a normed space because we don't have LCTVS yet, but everything is generalisable for free) and I stumble across a problem. The intrinsic interior/frontier/closure of A is defined to be the interior/frontier/closure of A taken as a set of its affine span.

import algebra.module.linear_map
import analysis.convex.topology
open set
variables {E : Type*} [normed_group E] [normed_space ℝ E] {x : E} {A B : set E}

def intrinsic_frontier (A : set E) :
  set E :=
coe '' (frontier {x : affine_span ℝ A | ↑x ∈ A})

def intrinsic_interior (A : set E) :
  set E :=
coe '' (interior {x : affine_span ℝ A | ↑x ∈ A})

def intrinsic_closure (A : set E) :
  set E :=
coe '' (closure {x : affine_span ℝ A | ↑x ∈ A})

I don't really want to define intrinsic_closure because it turns out that intrinsic_closure A = closure A as soon as E is finite dimensional. But things get weird in infinite dimension. In general we only have intrinsic_closure A ⊆ closure A. I can see a few ways to fix this:

1. Just stick with intrinsic_closure and have lemma intrinsic_closure_eq_closure [finite_dimensional E ℝ] : intrinsic_closure A = closure A
2. Change the definitions to

def intrinsic_frontier (A : set E) :
  set E :=
coe '' (frontier {x : closure (affine_span ℝ A : set E) | ↑x ∈ A})

def intrinsic_interior (A : set E) :
  set E :=
coe '' (interior {x : closure (affine_span ℝ A : set E) | ↑x ∈ A})

3. Change the definition of intrinsic_frontier to

def intrinsic_frontier (A : set E) :
  set E :=
closure A \ intrinsic_interior A

4. Change the definition of intrinsic_interior to

def intrinsic_interior (A : set E) :
  set E :=
closure A \ intrinsic_frontier A

I don't really know which is the most sensible option. I mostly want out of the definitions the facts that:

1. interior A ⊆ intrinsic_interior A
2. intrinsic_frontier A ⊆ frontier A
3. A.nonempty → (intrinsic_interior A).nonempty
   Any opinion anyone?