PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Transverse intersections of coordinate slices have the expected local form

Statement

Let $U \subseteq R^{m}$ be open. Suppose $S, T \subseteq U$ are given near a point $a \in S \cap T$ by independent coordinate slices: after a permutation of coordinates, there are smooth submersions $Φ : U \to R^{c}$ and $Ψ : U \to R^{d}$ with $S = Φ^{- 1} (0)$ , $T = Ψ^{- 1} (0)$ near $a$ , and with $d Φ_{a} \oplus d Ψ_{a} : T_{a} U \to R^{c} \times R^{d}$ surjective. Then $S \cap T$ is, near $a$ , an embedded submanifold of codimension $c + d$ ; in suitable local coordinates it is a coordinate slice.

Facts & Assumptions

Given: Open $U \subseteq R^{m}$ , submersions $Φ, Ψ$ , and a point $a \in S \cap T$ with the stated surjectivity.

[F1]

A local defining map records a submersion whose zero fibre is the local submanifold (Local defining maps for embedded submanifolds).

[L1]

The product of the two target maps is the unique map into the product with the prescribed components (A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice).

[L2]

A regular level set of a smooth map is an embedded submanifold (A regular level set is an embedded submanifold).

[L3]

For a Euclidean smooth map, the locus where the differential has rank at least a fixed value is open (Differential rank is lower semicontinuous).

Proof

technique · direct

1.1

By [L1], define $H : U \to R^{c} \times R^{d}$ by $H (x) = (Φ (x), Ψ (x))$ . Then $H^{- 1} (0, 0) = S \cap T$ near $a$ by [F1]. The differential of $H$ at $a$ is exactly $d Φ_{a} \oplus d Ψ_{a}$ , so it is surjective by hypothesis.

F1L1given

2.1

Since the target of $H$ has dimension $c + d$ , step 1.1 says $rank d H_{a} = c + d$ . By [L3], after shrinking to an open neighbourhood $W$ of $a$ , every point of $W$ has differential rank at least $c + d$ , hence exactly $c + d$ . Therefore every point of $W \cap H^{- 1} (0, 0)$ is regular for $H ∣_{W}$ , so $(0, 0)$ is a regular value of $H ∣_{W}$ .

L3step 1.1

3.1

By [L2], the common zero set $W \cap S \cap T = W \cap H^{- 1} (0, 0)$ is an embedded submanifold of codimension $c + d$ and therefore is locally a coordinate slice.

L2step 2.1

4.1

This is the claimed local form of the transverse intersection.

step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John M. Lee, Introduction to Smooth Manifolds, Embedded Submanifolds (standard reference, not scraped)