Finite line-arrangement subdivisions of plane graphs

This file supplies the source-side subdivision used in Moise Chapter 6, Theorem 2. A finite plane graph is encoded as one auxiliary broken line which traverses every edge (with harmless connector segments between edges). The line arrangement of that auxiliary chain resolves every source edge. Keeping only arrangement faces subordinate to an original face produces an honest subdivision of the graph.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.normalized_ge_of_line_nonneg {a b q t : ℝ} (hΔ : 0 < b - a) (hq : 0 ≤ q - ((1 - t) * a + t * b)) : t ≤ (b - a)⁻¹ * (q - a)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.normalized_le_of_line_nonpos {a b q t : ℝ} (hΔ : 0 < b - a) (hq : q - ((1 - t) * a + t * b) ≤ 0) : (b - a)⁻¹ * (q - a) ≤ t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.normalized_le_of_line_nonneg_of_neg {a b q t : ℝ} (hΔ : b - a < 0) (hq : 0 ≤ q - ((1 - t) * a + t * b)) : (b - a)⁻¹ * (q - a) ≤ t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.normalized_ge_of_line_nonpos_of_neg {a b q t : ℝ} (hΔ : b - a < 0) (hq : q - ((1 - t) * a + t * b) ≤ 0) : t ≤ (b - a)⁻¹ * (q - a)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeFace (K : PlaneComplex) : Type

The EdgeFace declaration.

Equations

• K.EdgeFace = ↥K.edges

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeEquiv (K : PlaneComplex) : K.EdgeFace ≃ Fin (Fintype.card K.EdgeFace)

The edgeEquiv declaration.

Equations

• K.edgeEquiv = Fintype.equivFin K.EdgeFace

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeAt (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : K.EdgeFace

The edgeAt declaration.

Equations

• K.edgeAt i = K.edgeEquiv.symm i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.vertexEquiv (K : PlaneComplex) : K.Vertex ≃ Fin (Fintype.card K.Vertex)

The vertexEquiv declaration.

Equations

• K.vertexEquiv = Fintype.equivFin K.Vertex

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.vertexAt (K : PlaneComplex) (i : Fin (Fintype.card K.Vertex)) : K.Vertex

The vertexAt declaration.

Equations

• K.vertexAt i = K.vertexEquiv.symm i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeAt_card (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : (↑(K.edgeAt i)).card = 2

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeFirst (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : K.Vertex

The edgeFirst declaration.

Equations

• K.edgeFirst i = ⋯.choose

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeSecond (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : K.Vertex

The edgeSecond declaration.

Equations

• K.edgeSecond i = ⋯.choose

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeFirst_ne_edgeSecond (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeFirst i ≠ K.edgeSecond i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeAt_eq (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : ↑(K.edgeAt i) = {K.edgeFirst i, K.edgeSecond i}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeAt_mem_simplexes (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : ↑(K.edgeAt i) ∈ K.simplexes

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeParameter (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : Plane →ᵃ[ℝ] ℝ

Affine coordinate from 0 to 1 on an enumerated source edge.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeParameter_apply_first (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : (K.edgeParameter i) (K.position (K.edgeFirst i)) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeParameter_apply_second (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : (K.edgeParameter i) (K.position (K.edgeSecond i)) = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeParameter_lineMap (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) (t : ℝ) : (K.edgeParameter i) ((AffineMap.lineMap (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))) t) = t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeParameter_mem_Icc (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) {x : Plane} (hx : x ∈ K.cellCarrier ↑(K.edgeAt i)) : (K.edgeParameter i) x ∈ Set.Icc 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.lineMap_edgeParameter_eq (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) {x : Plane} (hx : x ∈ K.cellCarrier ↑(K.edgeAt i)) : (AffineMap.lineMap (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))) ((K.edgeParameter i) x) = x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_edgeAt (K : PlaneComplex) (e : K.EdgeFace) : ∃ (i : Fin (Fintype.card K.EdgeFace)), K.edgeAt i = e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_vertexAt (K : PlaneComplex) (v : K.Vertex) : ∃ (i : Fin (Fintype.card K.Vertex)), K.vertexAt i = v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeChain (K : PlaneComplex) : BrokenLineData Set.univ

The auxiliary chain has one genuine edge segment at every even index; odd segments merely connect one enumerated edge to the next and are discarded by subordinateTo.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeChain_vertex_even (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeChain.vertex ⟨2 * ↑i, ⋯⟩ = K.position (K.edgeFirst i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeChain_vertex_odd (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeChain.vertex ⟨2 * ↑i + 1, ⋯⟩ = K.position (K.edgeSecond i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeChain_vertex_original (K : PlaneComplex) (i : Fin (Fintype.card K.Vertex)) : K.edgeChain.vertex ⟨2 * Fintype.card K.EdgeFace + ↑i, ⋯⟩ = K.position (K.vertexAt i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeChainIndex (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : Fin K.edgeChain.n

The edgeChainIndex declaration.

Equations

• K.edgeChainIndex i = ⟨2 * ↑i, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeChainIndex_castSucc (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : (K.edgeChainIndex i).castSucc = ⟨2 * ↑i, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeChainIndex_succ (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : (K.edgeChainIndex i).succ = ⟨2 * ↑i + 1, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeChain_segment (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : segment ℝ (K.edgeChain.vertex (K.edgeChainIndex i).castSucc) (K.edgeChain.vertex (K.edgeChainIndex i).succ) = K.cellCarrier ↑(K.edgeAt i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeArrangement (K : PlaneComplex) : PlaneComplex

The ambient arrangement generated by all graph edges.

Equations

• K.edgeArrangement = K.edgeChain.arrangementMesh.toPlaneComplex

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeSubdivision (K : PlaneComplex) : PlaneComplex

The arrangement faces subordinate to the original graph.

Equations

• K.edgeSubdivision = K.edgeArrangement.subordinateTo K

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeSubdivision_support_eq (K : PlaneComplex) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) : K.edgeSubdivision.support = K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeSubdivision_subdivides (K : PlaneComplex) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) : K.edgeSubdivision.Subdivides K

Arbitrarily fine marked arrangements

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeSample (K : PlaneComplex) (cuts : ℕ) : Type

The EdgeSample declaration.

Equations

• K.EdgeSample cuts = (Fin (Fintype.card K.EdgeFace) × Fin (cuts + 2))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeSampleEquiv (K : PlaneComplex) (cuts : ℕ) : K.EdgeSample cuts ≃ Fin (Fintype.card (K.EdgeSample cuts))

The edgeSampleEquiv declaration.

Equations

• K.edgeSampleEquiv cuts = Fintype.equivFin (K.EdgeSample cuts)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeSamplePoint (K : PlaneComplex) (cuts : ℕ) (s : K.EdgeSample cuts) : Plane

The edgeSamplePoint declaration.

Equations

• K.edgeSamplePoint cuts s = (AffineMap.lineMap (K.position (K.edgeFirst s.1)) (K.position (K.edgeSecond s.1))) (↑↑s.2 / (↑cuts + 1))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeParameter_samplePoint (K : PlaneComplex) (cuts : ℕ) (s : K.EdgeSample cuts) : (K.edgeParameter s.1) (K.edgeSamplePoint cuts s) = ↑↑s.2 / (↑cuts + 1)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChain (K : PlaneComplex) (cuts : ℕ) : BrokenLineData Set.univ

The auxiliary edge chain enlarged by cuts equally spaced interior marks on every edge. The marks need not occur consecutively: their two coordinate lines are what refine the ambient arrangement.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChain_vertex_even (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) : (K.sampledEdgeChain cuts).vertex ⟨2 * ↑i, ⋯⟩ = K.position (K.edgeFirst i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChain_vertex_odd (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) : (K.sampledEdgeChain cuts).vertex ⟨2 * ↑i + 1, ⋯⟩ = K.position (K.edgeSecond i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChain_vertex_sample (K : PlaneComplex) (cuts : ℕ) (s : K.EdgeSample cuts) : (K.sampledEdgeChain cuts).vertex ⟨2 * Fintype.card K.EdgeFace + ↑((K.edgeSampleEquiv cuts) s), ⋯⟩ = K.edgeSamplePoint cuts s

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChainSampleIndex (K : PlaneComplex) (cuts : ℕ) (s : K.EdgeSample cuts) : Fin ((K.sampledEdgeChain cuts).n + 1)

The sampledEdgeChainSampleIndex declaration.

Equations

• K.sampledEdgeChainSampleIndex cuts s = ⟨2 * Fintype.card K.EdgeFace + ↑((K.edgeSampleEquiv cuts) s), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeArrangement_monochromatic_vertical (K : PlaneComplex) (cuts : ℕ) (s : K.EdgeSample cuts) : (K.sampledEdgeChain cuts).arrangementMesh.IsMonochromatic (BrokenLineData.verticalLine (K.edgeSamplePoint cuts s))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeArrangement_monochromatic_horizontal (K : PlaneComplex) (cuts : ℕ) (s : K.EdgeSample cuts) : (K.sampledEdgeChain cuts).arrangementMesh.IsMonochromatic (BrokenLineData.horizontalLine (K.edgeSamplePoint cuts s))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledFace_parameter_side (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) (r : Fin (cuts + 2)) {u : Finset (K.sampledEdgeChain cuts).arrangementMesh.Vertex} (hu : u ∈ (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex.simplexes) : (∀ v ∈ u, (K.edgeParameter i) ((K.sampledEdgeChain cuts).arrangementMesh.position v) ≤ ↑↑r / (↑cuts + 1)) ∨ ∀ v ∈ u, ↑↑r / (↑cuts + 1) ≤ (K.edgeParameter i) ((K.sampledEdgeChain cuts).arrangementMesh.position v)

Every arrangement face lies wholly on one side of every rational mark on an original edge, when measured in that edge's affine coordinate.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledFaceCarrier_parameter_side (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) (r : Fin (cuts + 2)) {u : Finset (K.sampledEdgeChain cuts).arrangementMesh.Vertex} (hu : u ∈ (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex.simplexes) : (∀ x ∈ (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex.cellCarrier u, (K.edgeParameter i) x ≤ ↑↑r / (↑cuts + 1)) ∨ ∀ x ∈ (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex.cellCarrier u, ↑↑r / (↑cuts + 1) ≤ (K.edgeParameter i) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledFace_parameter_diameter (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) {u : Finset (K.sampledEdgeChain cuts).arrangementMesh.Vertex} (hu : u ∈ (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex.simplexes) (hui : (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex.cellCarrier u ⊆ K.cellCarrier ↑(K.edgeAt i)) {x y : Plane} (hx : x ∈ (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex.cellCarrier u) (hy : y ∈ (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex.cellCarrier u) : |(K.edgeParameter i) x - (K.edgeParameter i) y| ≤ 1 / (↑cuts + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChain_vertex_original (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.Vertex)) : (K.sampledEdgeChain cuts).vertex ⟨2 * Fintype.card K.EdgeFace + Fintype.card (K.EdgeSample cuts) + ↑i, ⋯⟩ = K.position (K.vertexAt i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChainIndex (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) : Fin (K.sampledEdgeChain cuts).n

The sampledEdgeChainIndex declaration.

Equations

• K.sampledEdgeChainIndex cuts i = ⟨2 * ↑i, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChainIndex_castSucc (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) : (K.sampledEdgeChainIndex cuts i).castSucc = ⟨2 * ↑i, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChainIndex_succ (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) : (K.sampledEdgeChainIndex cuts i).succ = ⟨2 * ↑i + 1, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeChain_segment (K : PlaneComplex) (cuts : ℕ) (i : Fin (Fintype.card K.EdgeFace)) : segment ℝ ((K.sampledEdgeChain cuts).vertex (K.sampledEdgeChainIndex cuts i).castSucc) ((K.sampledEdgeChain cuts).vertex (K.sampledEdgeChainIndex cuts i).succ) = K.cellCarrier ↑(K.edgeAt i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeArrangement (K : PlaneComplex) (cuts : ℕ) : PlaneComplex

The sampledEdgeArrangement declaration.

Equations

• K.sampledEdgeArrangement cuts = (K.sampledEdgeChain cuts).arrangementMesh.toPlaneComplex

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeSubdivision (K : PlaneComplex) (cuts : ℕ) : PlaneComplex

The sampledEdgeSubdivision declaration.

Equations

• K.sampledEdgeSubdivision cuts = (K.sampledEdgeArrangement cuts).subordinateTo K

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_sampledEdgeSubdivision_face_at (K : PlaneComplex) (cuts : ℕ) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) {x : Plane} (hxs : x ∈ K.cellCarrier s) : ∃ u ∈ (K.sampledEdgeSubdivision cuts).simplexes, x ∈ (K.sampledEdgeSubdivision cuts).cellCarrier u ∧ (K.sampledEdgeSubdivision cuts).cellCarrier u ⊆ K.cellCarrier s

Every point of an original graph face lies in a sampled-subdivision face contained in that same original face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeSubdivision_support_eq (K : PlaneComplex) (cuts : ℕ) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) : (K.sampledEdgeSubdivision cuts).support = K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_sampledEdgeSubdivision_vertex_position_eq (K : PlaneComplex) (cuts : ℕ) (v : K.Vertex) (hv : K.position v ∈ K.support) : ∃ (w : (K.sampledEdgeSubdivision cuts).Vertex), (K.sampledEdgeSubdivision cuts).position w = K.position v ∧ {w} ∈ (K.sampledEdgeSubdivision cuts).simplexes

Every original vertex position which lies in the graph support becomes an actual zero-face of the sampled subdivision. The extra original-vertex marks in sampledEdgeChain ensure this even when the original abstract vertex was not itself used by a face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sampledEdgeSubdivision_subdivides (K : PlaneComplex) (cuts : ℕ) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) : (K.sampledEdgeSubdivision cuts).Subdivides K

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeLengthBound (K : PlaneComplex) : ℝ

A positive common upper bound for the lengths of all enumerated edges.

Equations

• K.edgeLengthBound = 1 + ∑ i : Fin (Fintype.card K.EdgeFace), dist (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeLengthBound_pos (K : PlaneComplex) : 0 < K.edgeLengthBound

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edge_length_lt_bound (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) : dist (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i)) < K.edgeLengthBound

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_sampledEdgeSubdivision_image_diameter_lt (K : PlaneComplex) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) {h : Plane → Plane} (hcont : ContinuousOn h K.support) {η : ℝ} (hη : 0 < η) : ∃ (cuts : ℕ), ∀ u ∈ (K.sampledEdgeSubdivision cuts).simplexes, ∀ x ∈ (K.sampledEdgeSubdivision cuts).cellCarrier u, ∀ y ∈ (K.sampledEdgeSubdivision cuts).cellCarrier u, dist (h x) (h y) < η

Heine--Cantor plus the marked line arrangement: every finite embedded graph has a subordinate subdivision whose faces have arbitrarily small image diameter under a continuous map.