Zulip Chat Archive

Stream: maths

Topic: intrinsic interior/frontier/closure


view this post on Zulip 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