# Zulip Chat Archive

## 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:

- Just stick with
`intrinsic_closure`

and have`lemma intrinsic_closure_eq_closure [finite_dimensional E ℝ] : intrinsic_closure A = closure A`

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

- Change the definition of
`intrinsic_frontier`

to

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

- 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:

`interior A ⊆ intrinsic_interior A`

`intrinsic_frontier A ⊆ frontier A`

`A.nonempty → (intrinsic_interior A).nonempty`

Any opinion anyone?

Last updated: Jun 17 2021 at 18:14 UTC