## Stream: maths

### Topic: intrinsic interior/frontier/closure

#### Yaël Dillies (Apr 19 2021 at 15:21):

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})

1. Change the definition of intrinsic_frontier to
def intrinsic_frontier (A : set E) :
set E :=
closure A \ intrinsic_interior A

1. 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?

Last updated: Jun 17 2021 at 18:14 UTC