Fine subdivisions of finite plane complexes

Moise Chapter 6 repeatedly chooses a subdivision sufficiently fine for a continuous map. For a finite plane complex this follows from a concrete finite line arrangement: cover the compact support by small balls and, around every center, cut by two vertical and two horizontal lines. Every chamber meeting the corresponding smaller ball is trapped in the resulting rectangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.affine_nonneg_on_cellCarrier (K : PlaneComplex) {a : Plane →ᵃ[ℝ] ℝ} {s : Finset K.Vertex} (hs : ∀ v ∈ s, 0 ≤ a (K.position v)) (x : Plane) : x ∈ K.cellCarrier s → 0 ≤ a x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.affine_nonpos_on_cellCarrier (K : PlaneComplex) {a : Plane →ᵃ[ℝ] ℝ} {s : Finset K.Vertex} (hs : ∀ v ∈ s, a (K.position v) ≤ 0) (x : Plane) : x ∈ K.cellCarrier s → a x ≤ 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.verticalCut (c : ℝ) : Plane →ᵃ[ℝ] ℝ

The vertical line whose zero set is x = c.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.horizontalCut (c : ℝ) : Plane →ᵃ[ℝ] ℝ

The horizontal line whose zero set is y = c.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.verticalCut_apply (c : ℝ) (p : Plane) : (verticalCut c) p = p.ofLp 0 - c

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.horizontalCut_apply (c : ℝ) (p : Plane) : (horizontalCut c) p = p.ofLp 1 - c

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.boxCuts (p : Plane) (r : ℝ) : List (Plane →ᵃ[ℝ] ℝ)

Four coordinate cuts bounding a square of radius r around p.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.mem_boxCuts {p : Plane} {r : ℝ} {a : Plane →ᵃ[ℝ] ℝ} : a ∈ boxCuts p r ↔ a = verticalCut (p.ofLp 0 - r) ∨ a = verticalCut (p.ofLp 0 + r) ∨ a = horizontalCut (p.ofLp 1 - r) ∨ a = horizontalCut (p.ofLp 1 + r)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.coverCuts (centers : Finset Plane) (r : ℝ) : List (Plane →ᵃ[ℝ] ℝ)

All box cuts associated to a finite set of centers.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.boxCut_mem_coverCuts {centers : Finset Plane} {p : Plane} (hp : p ∈ centers) (r : ℝ) {a : Plane →ᵃ[ℝ] ℝ} (ha : a ∈ boxCuts p r) : a ∈ coverCuts centers r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.cellCarrier_subset_box_of_monochromatic (N : TriangleMesh) {p : Plane} {r : ℝ} (hr : 0 < r) (hmono : ∀ a ∈ boxCuts p r, N.IsMonochromatic a) {t : Finset N.Vertex} (ht : t ∈ N.triangles) {x : Plane} (hx : x ∈ N.toPlaneComplex.cellCarrier t) (hxp : dist x p < r / 2) (y : Plane) : y ∈ N.toPlaneComplex.cellCarrier t → p.ofLp 0 - r ≤ y.ofLp 0 ∧ y.ofLp 0 ≤ p.ofLp 0 + r ∧ p.ofLp 1 - r ≤ y.ofLp 1 ∧ y.ofLp 1 ≤ p.ofLp 1 + r

A chamber cut by the four box lines around p is trapped in that box as soon as it meets the concentric half-radius ball.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_subdivision_image_dist_lt (K : PlaneComplex) (hpure : K.IsPure2) {h : Plane → Plane} (hcont : ContinuousOn h K.support) {eps : ℝ} (heps : 0 < eps) : ∃ (L : PlaneComplex), L.IsPure2 ∧ L.Subdivides K ∧ ∀ t ∈ L.cells, ∀ x ∈ L.cellCarrier t, ∀ y ∈ L.cellCarrier t, dist (h x) (h y) < eps

A finite pure plane complex has a subdivision on whose two-cells a prescribed continuous map has arbitrarily small oscillation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_subdivision_subordinate_openCover (K : PlaneComplex) (hpure : K.IsPure2) {I : Type u_1} (U : I → Set Plane) (hU : ∀ (i : I), IsOpen (U i)) (hcover : K.support ⊆ ⋃ (i : I), U i) : ∃ (L : PlaneComplex), L.IsPure2 ∧ L.Subdivides K ∧ ∀ t ∈ L.cells, ∃ (i : I), L.cellCarrier t ⊆ U i

A sufficiently fine subdivision of a pure finite plane complex is subordinate to any open cover of its support.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.OpenSubmesh (K : PlaneComplex) (C U : Set Plane) : Type 1

A finite triangle submesh selected between a compact set and an ambient open set. Unlike a full subdivision, its support is only the retained compact polyhedron; every retained triangle is nevertheless subordinate to the original plane complex.

• mesh : TriangleMesh

  The mesh declaration.

• face_subordinate (t : Finset self.mesh.Vertex) : t ∈ self.mesh.triangles → ∃ s ∈ K.simplexes, self.mesh.toPlaneComplex.cellCarrier t ⊆ K.cellCarrier s
• covers : C ⊆ self.mesh.toPlaneComplex.support
• contained : self.mesh.toPlaneComplex.support ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.OpenSubmesh.support_subset_original {K : PlaneComplex} {C U : Set Plane} (L : K.OpenSubmesh C U) : L.mesh.toPlaneComplex.support ⊆ K.support

Every retained triangle of an open submesh still lies in the original complex support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_openSubmesh (K : PlaneComplex) (hpure : K.IsPure2) {C U : Set Plane} (hC : IsCompact C) (hCK : C ⊆ K.support) (hU : IsOpen U) (hCU : C ⊆ U) : Nonempty (K.OpenSubmesh C U)

Every compact subset of an open subset of a pure finite plane complex is covered by a finite triangle submesh lying in that open set.