Nested safe midpoint stages of an open polyhedron

For an open subset U of a finite intrinsic complex, retain at level n every midpoint triangle whose whole carrier is contained in U. These finite stages are nested and exhaust U. They are the finite layers used in Moise Chapter 8, Theorem 2 before adjacent frontier subdivisions are reconciled by coning.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeSubdivision (K : IntrinsicTwoComplex) (n : ℕ) : K.Subdivision

The n-fold midpoint subdivision used at one safe stage.

Equations

• K.safeSubdivision n = K.iteratedMidpointSubdivision n

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeFaces (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : Finset (Finset (K.safeSubdivision n).refined.Vertex)

Refined triangles whose complete transported carriers lie in the prescribed open set.

Equations

• K.safeFaces U n = {t ∈ (K.safeSubdivision n).refined.faces | ∀ x ∈ (K.safeSubdivision n).refined.faceCarrier t, (K.safeSubdivision n).homeo x ∈ U}

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeFacesDecidablePred (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : DecidablePred fun (t : Finset (K.safeSubdivision n).refined.Vertex) => t ∈ K.safeFaces U n

Equations

• K.safeFacesDecidablePred U n t = Finset.decidableMem t (K.safeFaces U n)

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeStage (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : IntrinsicTwoComplex

The finite intrinsic subcomplex retained at level n.

Equations

• K.safeStage U n = (K.safeSubdivision n).refined.restrictFaces fun (t : Finset (K.safeSubdivision n).refined.Vertex) => t ∈ K.safeFaces U n

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeStageInclusion (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : (K.safeStage U n).realization → K.realization

Include a safe stage into the original finite realization.

Equations

• K.safeStageInclusion U n = ⇑(K.safeSubdivision n).homeo ∘ (K.safeSubdivision n).refined.restrictFacesInclusion fun (t : Finset (K.safeSubdivision n).refined.Vertex) => t ∈ K.safeFaces U n

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isEmbedding_safeStageInclusion (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : Topology.IsEmbedding (K.safeStageInclusion U n)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeStageSupport (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : Set K.realization

Carrier of one finite safe stage in the original realization.

Equations

• K.safeStageSupport U n = Set.range (K.safeStageInclusion U n)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isCompact_safeStageSupport (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : IsCompact (K.safeStageSupport U n)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeStageSupport_subset (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : K.safeStageSupport U n ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeStageSupport_mono (K : IntrinsicTwoComplex) (U : Set K.realization) (n : ℕ) : K.safeStageSupport U n ⊆ K.safeStageSupport U (n + 1)

Every point of a retained old triangle is carried by a retained child at the next midpoint level.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeStageSupport_mono_of_le (K : IntrinsicTwoComplex) (U : Set K.realization) {n m : ℕ} (hnm : n ≤ m) : K.safeStageSupport U n ⊆ K.safeStageSupport U m

Safe-stage supports are monotone in the subdivision level.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_safeStageSupport_of_mem (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) {p : K.realization} (hp : p ∈ U) : ∃ (n : ℕ), p ∈ K.safeStageSupport U n

A point of an open set is eventually carried by a safe midpoint triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_interior_safeStageSupport_of_mem (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) {p : K.realization} (hp : p ∈ U) : ∃ (n : ℕ), p ∈ interior (K.safeStageSupport U n)

Every point of an open set eventually lies in the ambient interior of a finite safe stage. This is stronger than mere exhaustion and is the compact-control input for the locally finite shell construction.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_safeStageSupport_interior_of_compact (K : IntrinsicTwoComplex) (U : Set K.realization) {C : Set K.realization} (hC : IsCompact C) (hU : IsOpen U) (hCU : C ⊆ U) : ∃ (n : ℕ), C ⊆ interior (K.safeStageSupport U n)

A compact subset of an open polyhedron is eventually contained in the interior of one finite safe stage.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.nextSafeStage (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : ℕ

A later midpoint level whose safe support contains the given safe support in its interior. The maximum with n + 1 makes the selected levels strictly increase.

Equations

• K.nextSafeStage U hU n = max (Classical.choose ⋯) (n + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.lt_nextSafeStage (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : n < K.nextSafeStage U hU n

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeStageSupport_subset_interior_next (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : K.safeStageSupport U n ⊆ interior (K.safeStageSupport U (K.nextSafeStage U hU n))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustionIndex (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) : ℕ → ℕ

Cofinal levels selected so that consecutive finite supports are nested through interiors.

Equations

• K.safeExhaustionIndex U hU 0 = 0
• K.safeExhaustionIndex U hU n.succ = K.nextSafeStage U hU (K.safeExhaustionIndex U hU n)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustionIndex_zero (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) : K.safeExhaustionIndex U hU 0 = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustionIndex_succ (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : K.safeExhaustionIndex U hU (n + 1) = K.nextSafeStage U hU (K.safeExhaustionIndex U hU n)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustionIndex_lt_succ (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : K.safeExhaustionIndex U hU n < K.safeExhaustionIndex U hU (n + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.id_le_safeExhaustionIndex (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : n ≤ K.safeExhaustionIndex U hU n

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustionIndex_mono (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) {n m : ℕ} (hnm : n ≤ m) : K.safeExhaustionIndex U hU n ≤ K.safeExhaustionIndex U hU m

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustion (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : Set K.realization

The selected compact exhaustion stage.

Equations

• K.safeExhaustion U hU n = K.safeStageSupport U (K.safeExhaustionIndex U hU n)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isCompact_safeExhaustion (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : IsCompact (K.safeExhaustion U hU n)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustion_subset (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : K.safeExhaustion U hU n ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustion_subset_interior_succ (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : K.safeExhaustion U hU n ⊆ interior (K.safeExhaustion U hU (n + 1))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustion_mono (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (n : ℕ) : K.safeExhaustion U hU n ⊆ K.safeExhaustion U hU (n + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeExhaustion_mono_of_le (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) {n m : ℕ} (hnm : n ≤ m) : K.safeExhaustion U hU n ⊆ K.safeExhaustion U hU m

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.iUnion_safeExhaustion (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) : ⋃ (n : ℕ), K.safeExhaustion U hU n = U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.iUnion_interior_safeExhaustion (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) : ⋃ (n : ℕ), interior (K.safeExhaustion U hU n) = U

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.safeShell (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) : ℕ → Set ↑U

The compact shells of the selected exhaustion, regarded in the open subspace. Shell zero is the first compact stage; shell n + 1 is the next stage with the interior of stage n removed.

Equations

• K.safeShell U hU 0 = Subtype.val ⁻¹' K.safeExhaustion U hU 0
• K.safeShell U hU n.succ = Subtype.val ⁻¹' (K.safeExhaustion U hU (n + 1) \ interior (K.safeExhaustion U hU n))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.locallyFinite_safeShell (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) : LocallyFinite (K.safeShell U hU)

The exhaustion shells are locally finite in U. They may accumulate at the frontier in the original compact realization, which is precisely why the ambient space here is the open subspace.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.iUnion_safeStageSupport (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) : ⋃ (n : ℕ), K.safeStageSupport U n = U

The nested finite safe stages cover exactly the prescribed open set.