783: For C∞ Manifold, Subset, and Point on Subset, if Chart Satisfies Local Slice Condition for Embedded Submanifold or Local Slice Condition for Embedded Submanifold with Boundary, Its Sub-Open-Neighborhood Does So

<The previous article in this series | The table of contents of this series | The next article in this series>

description/proof of that for $C^{\mathrm{\infty }}$ manifold, subset, and point on subset, if chart satisfies local slice condition for embedded submanifold or local slice condition for embedded submanifold with boundary, its sub-open-neighborhood does so

---

Topics

About: $C^{\mathrm{\infty }}$ manifold

---

The table of contents of this article

• Starting Context
• Target Context
• Orientation
• Main Body
• 1: Structured Description
• 2: Natural Language Description
• 3: Proof

---

Starting Context

• The reader knows a definition of $C^{\mathrm{\infty }}$ manifold.
• The reader admits the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid.

---

Target Context

• The reader will have a description and a proof of the proposition that for any $C^{\mathrm{\infty }}$ manifold, any subset, and any point on the subset, if a chart satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary, its any sub-open-neighborhood does so.

---

Orientation

There is a list of definitions discussed so far in this site.

There is a list of propositions discussed so far in this site.

---

Main Body

---

1: Structured Description

Here is the rules of Structured Description.

Entities:
$M^{\prime }$: $\in \{\text{ the }{d}^{\prime }\text{ -dimensional }{C}^{\mathrm{\infty }}\text{ manifolds }\}$
$S$: $\subseteq M^{\prime }$
$J$: $\subseteq \{1,...,d^{\prime }\}$ such that $|J|=d$
$k$: $\in J$
$s$: $\in S$
${\lambda }_{J,r}$: $:Pow({\mathbb{R}}^{d^{\prime }})\to Pow({\mathbb{R}}^{d^{\prime }})$, $=\text{ the slicing map }$, where $r\in {\mathbb{R}}^{d^{\prime }}$ is any
${\lambda }_{J,r,k}$: $:Pow({\mathbb{R}}^{d^{\prime }})\to Pow({\mathbb{R}}^{d^{\prime }})$, $=\text{ the slicing-and-halving map }$, where $r\in {\mathbb{R}}^{d^{\prime }}$ is any
${\pi }_J$: $:{\mathbb{R}}^{d^{\prime }}\to {\mathbb{R}}^d$, $=\text{ the projection }$
$(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$: $\in \{\text{ the charts around }s\text{ of }{M}^{\prime }\}$
$V_s^{\prime }$: $\in \{\text{ the open neighborhoods of }s\text{ on }{M}^{\prime }\}$, such that $V_s^{\prime }\subseteq U_s^{\prime }$
//

Statements:
$(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$ satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary
$⟹$
$(V_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime }{|}_{V_s^{\prime }})$ satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary
//

---

2: Natural Language Description

For any $d^{\prime }$-dimensional $C^{\mathrm{\infty }}$ manifold, $M^{\prime }$, any subset, $S\subseteq M^{\prime }$, any subset, $J\subseteq \{1,...,d^{\prime }\}$, such that $|J|=d$, any $k\in J$, any point, $s\in S$, the slicing map, ${\lambda }_{J,r}:Pow({\mathbb{R}}^{d^{\prime }})\to Pow({\mathbb{R}}^{d^{\prime }})$, where $r\in {\mathbb{R}}^{d^{\prime }}$ is any, the slicing-and-halving map, ${\lambda }_{J,r,k}:Pow({\mathbb{R}}^{d^{\prime }})\to Pow({\mathbb{R}}^{d^{\prime }})$, where $r\in {\mathbb{R}}^{d^{\prime }}$ is any, the projection, ${\pi }_J:{\mathbb{R}}^{d^{\prime }}\to {\mathbb{R}}^d$, any chart around $s$, $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$, and any open neighborhood of $s$, $V_s^{\prime }\subseteq M^{\prime }$, such that $V_s^{\prime }\subseteq U_s^{\prime }$, if $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$ satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary, $(V_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime }{|}_{V_s^{\prime }})$ satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary.

---

3: Proof

Whole Strategy: Step 1: suppose that $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$ satisfies the local slice condition for embedded submanifold and get the formalization, ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$; Step 2: see that ${\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))$ is satisfied; Step 3: suppose that $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$ satisfies the local slice condition for embedded submanifold with boundary and get the formalization, ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))\vee ({\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime })))$; Step 4: see that ${\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))\vee ({\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(V_s^{\prime })))$ is satisfied.

Step 1:

Let us suppose that $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$ satisfies the local slice condition for embedded submanifold.

By the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid, ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$.

Step 2:

By the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid, all what we need to see is that ${\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))$ is satisfied.

Let $p\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)$ be any and see that $p\in {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))$.

$p\in {\varphi }_s^{\prime }(V_s^{\prime })$, because $p\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)\subseteq {\varphi }_s^{\prime }(V_s^{\prime })$.

$p\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)\subseteq {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$, which implies that for each $j\in \{1,...,d^{\prime }\}\setminus J$, $p^j={\varphi }_s^{\prime }(s{)}^j$. But that implies that $p\in {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))$.

Let $p\in {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))$ be any and see that $p\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)$.

There is a $p^{\prime }\in V_s^{\prime }$ such that $p={\varphi }_s^{\prime }(p^{\prime })$.

$p\in {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))\subseteq {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))={\varphi }_s^{\prime }(U_s^{\prime }\cap S)$. So, there is a $p^{″}\in U_s^{\prime }\cap S$ such that $p={\varphi }_s^{\prime }(p^{″})$.

As ${\varphi }_s^{\prime }$ is injective, $p^{\prime }=p^{″}\in V_s^{\prime }\cap U_s^{\prime }\cap S=V_s^{\prime }\cap S$. So, $p={\varphi }_s^{\prime }(p^{\prime })\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)$.

So, ${\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))$.

Step 3:

Let us suppose that $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$ satisfies the local slice condition for embedded submanifold with boundary.

By the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid, ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))\vee ({\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime })))$.

Step 4:

By the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid, all what we need to see is that ${\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))\vee ({\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(V_s^{\prime })))$ is satisfied.

When ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$, ${\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(V_s^{\prime }))$, as before.

Let us suppose that ${\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))$ and see that ${\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(V_s^{\prime }))$.

${\varphi }_s^{\prime }(s{)}^k=0$, obviously.

Let $p\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)$ be any and see that $p\in {\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(V_s^{\prime }))$.

$p\in {\varphi }_s^{\prime }(V_s^{\prime })$, because $p\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)\subseteq {\varphi }_s^{\prime }(V_s^{\prime })$.

$p\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)\subseteq {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))$, which implies that for each $j\in \{1,...,d^{\prime }\}\setminus J$, $p^j={\varphi }_s^{\prime }(s{)}^j$ and ${\varphi }_s^{\prime }(s{)}^k\le p^k$. But that implies that $p\in {\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(V_s^{\prime }))$.

Let $p\in {\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(V_s^{\prime }))$ be any and see that $p\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)$.

There is a $p^{\prime }\in V_s^{\prime }$ such that $p={\varphi }_s^{\prime }(p^{\prime })$.

$p\in {\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(V_s^{\prime }))\subseteq {\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))={\varphi }_s^{\prime }(U_s^{\prime }\cap S)$. So, there is a $p^{″}\in U_s^{\prime }\cap S$ such that $p={\varphi }_s^{\prime }(p^{″})$.

As ${\varphi }_s^{\prime }$ is injective, $p^{\prime }=p^{″}\in V_s^{\prime }\cap U_s^{\prime }\cap S=V_s^{\prime }\cap S$. So, $p={\varphi }_s^{\prime }(p^{\prime })\in {\varphi }_s^{\prime }(V_s^{\prime }\cap S)$.

So, ${\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\varphi }_s^{\prime }(V_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(V_s^{\prime }))$.

---

References

<The previous article in this series | The table of contents of this series | The next article in this series>