Coning a subdivided triangle boundary

This file contains the finite geometry used in Moise Chapter 5. The central observation is that radial segments from an interior point of a convex set meet only as dictated by their endpoints on the frontier. It is the face-to-face lemma behind the cone extension of a PL map on a triangle boundary.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsTriangle.infinite_interior {C : Set Plane} (hC : IsTriangle C) : (interior C).Infinite

A nondegenerate plane triangle has infinitely many interior points.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsTriangle.convex {C : Set Plane} (hC : IsTriangle C) : Convex ℝ C

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsTriangle.isCompact {C : Set Plane} (hC : IsTriangle C) : IsCompact C

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsTriangle.frontier_nonempty {C : Set Plane} (hC : IsTriangle C) : (frontier C).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsTriangle.exists_interior_not_mem_range {C : Set Plane} (hC : IsTriangle C) {ι : Type u_1} [Finite ι] (p : ι → Plane) : ∃ c ∈ interior C, c ∉ Set.range p

An interior cone point can be chosen away from any prescribed finite family of points.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_frontier_endpoint {S : Set Plane} (hS : Convex ℝ S) (hcompact : IsCompact S) {c x : Plane} (hc : c ∈ interior S) (hx : x ∈ S) (hfrontier : (frontier S).Nonempty) : ∃ y ∈ frontier S, x ∈ segment ℝ c y

Every point of a compact convex body lies on a radial segment from an interior point to the frontier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.eq_of_mem_segment_interior_frontier {S : Set Plane} (hS : Convex ℝ S) {c x y z : Plane} (hc : c ∈ interior S) (hx : x ∈ frontier S) (hy : y ∈ frontier S) (hzx : z ∈ segment ℝ c x) (hzy : z ∈ segment ℝ c y) (hzc : z ≠ c) : x = y

Two radial segments from an interior point of a convex set cannot share a non-central point unless their frontier endpoints agree.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convexHull_insert_inter_convexHull_insert {S A B : Set Plane} (hS : Convex ℝ S) (hA : A.Nonempty) (hB : B.Nonempty) {c : Plane} (hc : c ∈ interior S) (hAS : (convexHull ℝ) A ⊆ frontier S) (hBS : (convexHull ℝ) B ⊆ frontier S) (hface : (convexHull ℝ) A ∩ (convexHull ℝ) B = (convexHull ℝ) (A ∩ B)) : (convexHull ℝ) (insert c A) ∩ (convexHull ℝ) (insert c B) = (convexHull ℝ) (insert c (A ∩ B))

Coning preserves a face-to-face intersection when the base faces lie in the frontier of a convex set and the cone point lies in its interior.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convexHull_insert_inter_convexHull {S A B : Set Plane} (hS : Convex ℝ S) (hA : A.Nonempty) {c : Plane} (hc : c ∈ interior S) (hAS : (convexHull ℝ) A ⊆ frontier S) (hBS : (convexHull ℝ) B ⊆ frontier S) (hface : (convexHull ℝ) A ∩ (convexHull ℝ) B = (convexHull ℝ) (A ∩ B)) : (convexHull ℝ) (insert c A) ∩ (convexHull ℝ) B = (convexHull ℝ) (A ∩ B)

The mixed cone/base face intersection used when exactly one face contains the cone point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convexHull_insert_inter_convexHull_insert' {S A B : Set Plane} (hS : Convex ℝ S) {c : Plane} (hc : c ∈ interior S) (hAS : (convexHull ℝ) A ⊆ frontier S) (hBS : (convexHull ℝ) B ⊆ frontier S) (hface : (convexHull ℝ) A ∩ (convexHull ℝ) B = (convexHull ℝ) (A ∩ B)) : (convexHull ℝ) (insert c A) ∩ (convexHull ℝ) (insert c B) = (convexHull ℝ) (insert c (A ∩ B))

Cone/cone intersection, including the degenerate case where one base face is empty.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convexHull_insert_inter_convexHull' {S A B : Set Plane} (hS : Convex ℝ S) {c : Plane} (hc : c ∈ interior S) (hAS : (convexHull ℝ) A ⊆ frontier S) (hBS : (convexHull ℝ) B ⊆ frontier S) (hface : (convexHull ℝ) A ∩ (convexHull ℝ) B = (convexHull ℝ) (A ∩ B)) : (convexHull ℝ) (insert c A) ∩ (convexHull ℝ) B = (convexHull ℝ) (A ∩ B)

Cone/base intersection, including an empty cone base.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.not_collinear_interior_frontier_segment {S : Set Plane} (hS : Convex ℝ S) {c a b : Plane} (hc : c ∈ interior S) (ha : a ∈ frontier S) (hb : b ∈ frontier S) (hab : a ≠ b) (hsegment : segment ℝ a b ⊆ frontier S) : ¬Collinear ℝ {c, a, b}

An interior point and the endpoints of a nondegenerate frontier segment are not collinear.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineIndependent_insert_interior_of_card_le_two {S : Set Plane} (hS : Convex ℝ S) {A : Finset Plane} (hAcard : A.card ≤ 2) (hAI : AffineIndependent ℝ Subtype.val) (hAS : (convexHull ℝ) ↑A ⊆ frontier S) {c : Plane} (hc : c ∈ interior S) : AffineIndependent ℝ Subtype.val

Adding an interior cone point to at most two affinely independent frontier vertices preserves affine independence.

@[reducible, inline]

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

Vertices which actually occur in the geometric support. Passing to this subtype removes irrelevant vertices that a PlaneComplex is allowed to carry.

Equations

• K.ActiveVertex = { v : K.Vertex // K.position v ∈ K.support }

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.activeVertexFintype (K : PlaneComplex) : Fintype K.ActiveVertex

Equations

• K.activeVertexFintype = Fintype.ofFinite K.ActiveVertex

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.activeEmbedding (K : PlaneComplex) : K.ActiveVertex ↪ K.Vertex

The activeEmbedding declaration.

Equations

• K.activeEmbedding = Function.Embedding.subtype fun (v : K.Vertex) => K.position v ∈ K.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.activeSimplexes (K : PlaneComplex) : Finset (Finset K.ActiveVertex)

The activeSimplexes declaration.

Equations

• K.activeSimplexes = {s : Finset K.ActiveVertex | Finset.map K.activeEmbedding s ∈ K.simplexes}

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_activeSimplexes (K : PlaneComplex) {s : Finset K.ActiveVertex} : s ∈ K.activeSimplexes ↔ Finset.map K.activeEmbedding s ∈ K.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.active_position_image (K : PlaneComplex) (s : Finset K.ActiveVertex) : (fun (v : K.ActiveVertex) => K.position ↑v) '' ↑s = K.position '' ↑(Finset.map K.activeEmbedding s)

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

Delete all unused vertices without changing the support or any face geometry.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.active_cellCarrier (K : PlaneComplex) (s : Finset K.ActiveVertex) : K.active.cellCarrier s = K.cellCarrier (Finset.map K.activeEmbedding s)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.active_support (K : PlaneComplex) : K.active.support = K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.IsPure2.active (K : PlaneComplex) (hpure : K.IsPure2) : K.active.IsPure2

Removing unused vertices preserves purity of a two-dimensional complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.card_le_two_of_support_eq_frontier (K : PlaneComplex) {S : Set Plane} (hSclosed : IsClosed S) (hsupport : K.support = frontier S) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) : s.card ≤ 2

A plane complex supported on the frontier of a closed set has no two-dimensional face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.active_subdivides_left {L K : PlaneComplex} (h : L.Subdivides K) : L.active.Subdivides K

@[reducible, inline]

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

Vertices which occur in at least one abstract face. Unlike ActiveVertex, this removes a vertex whose geometric position happens to lie in the support without being part of any face.

Equations

• K.UsedVertex = { v : K.Vertex // ∃ s ∈ K.simplexes, v ∈ s }

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.usedVertexFintype (K : PlaneComplex) : Fintype K.UsedVertex

Equations

• K.usedVertexFintype = Fintype.ofFinite K.UsedVertex

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.usedEmbedding (K : PlaneComplex) : K.UsedVertex ↪ K.Vertex

The usedEmbedding declaration.

Equations

• K.usedEmbedding = Function.Embedding.subtype fun (v : K.Vertex) => ∃ s ∈ K.simplexes, v ∈ s

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.usedSimplexes (K : PlaneComplex) : Finset (Finset K.UsedVertex)

The usedSimplexes declaration.

Equations

• K.usedSimplexes = {s : Finset K.UsedVertex | Finset.map K.usedEmbedding s ∈ K.simplexes}

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_usedSimplexes (K : PlaneComplex) {s : Finset K.UsedVertex} : s ∈ K.usedSimplexes ↔ Finset.map K.usedEmbedding s ∈ K.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.used_position_image (K : PlaneComplex) (s : Finset K.UsedVertex) : (fun (v : K.UsedVertex) => K.position ↑v) '' ↑s = K.position '' ↑(Finset.map K.usedEmbedding s)

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

Delete vertices unused by every face, without changing the represented complex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.used_cellCarrier (K : PlaneComplex) (s : Finset K.UsedVertex) : K.used.cellCarrier s = K.cellCarrier (Finset.map K.usedEmbedding s)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.used_support (K : PlaneComplex) : K.used.support = K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.used_vertex_face (K : PlaneComplex) (v : K.UsedVertex) : {v} ∈ K.used.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_used_face_eq (K : PlaneComplex) (s : Finset K.Vertex) (hs : s ∈ K.simplexes) : ∃ t ∈ K.used.simplexes, Finset.map K.usedEmbedding t = s ∧ K.used.cellCarrier t = K.cellCarrier s

Every face of a complex is represented by an identical geometric face after unused vertices are removed.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.IsPure2.used (K : PlaneComplex) (hpure : K.IsPure2) : K.used.IsPure2

Removing vertices unused by every face preserves two-dimensional purity.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.used_subdivides_left {L K : PlaneComplex} (h : L.Subdivides K) : L.used.Subdivides K

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_affineMap_eqOn_affineIndependent {ι : Type u_1} [Nonempty ι] (p q : ι → Plane) (hp : AffineIndependent ℝ p) : ∃ (g : Plane →ᵃ[ℝ] Plane), ∀ (i : ι), g (p i) = q i

Values prescribed on an affinely independent family extend to an affine map of the plane.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapGraph (K : PlaneComplex) (f : Plane → Plane) (hvertex : ∀ (v : K.Vertex), K.position v ∈ K.support) (hinj : Set.InjOn f K.support) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) : PlaneComplex

Map a one-dimensional complex by a function affine on every face and injective on its support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapGraph_cellCarrier (K : PlaneComplex) (f : Plane → Plane) (hvertex : ∀ (v : K.Vertex), K.position v ∈ K.support) (hinj : Set.InjOn f K.support) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) : (K.mapGraph f hvertex hinj hgraph haffine).cellCarrier s = f '' K.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapGraph_support (K : PlaneComplex) (f : Plane → Plane) (hvertex : ∀ (v : K.Vertex), K.position v ∈ K.support) (hinj : Set.InjOn f K.support) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) : (K.mapGraph f hvertex hinj hgraph haffine).support = f '' K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapGraph_baryEval_eq (K : PlaneComplex) (f : Plane → Plane) (hvertex : ∀ (v : K.Vertex), K.position v ∈ K.support) (hinj : Set.InjOn f K.support) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) {z : K.Vertex → ℝ} (hzsupp : ∀ v ∉ s, z v = 0) (hz0 : ∀ (v : K.Vertex), 0 ≤ z v) (hzsum : ∑ v : K.Vertex, z v = 1) : (K.mapGraph f hvertex hinj hgraph haffine).baryEval z = f (K.baryEval z)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.realizationHomeomorphAll (K : PlaneComplex) : ↑(GeometricRealization K.Vertex K.simplexes) ≃ₜ ↑K.support

The canonical barycentric homeomorphism using all simplexes, with no purity hypothesis.

Equations

• K.realizationHomeomorphAll = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.realizationHomeomorphAll_apply (K : PlaneComplex) (x : ↑(GeometricRealization K.Vertex K.simplexes)) : ↑(K.realizationHomeomorphAll x) = K.baryEval ↑x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.reposition (K : PlaneComplex) (position' : K.Vertex → Plane) (hinj : Function.Injective position') (haff : ∀ s ∈ K.simplexes, AffineIndependent ℝ fun (v : ↥s) => position' ↑v) (hface : ∀ s ∈ K.simplexes, ∀ t ∈ K.simplexes, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) : PlaneComplex

Reposition a plane complex while retaining its abstract simplexes.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.repositionHomeomorphAll (K : PlaneComplex) (position' : K.Vertex → Plane) (hinj : Function.Injective position') (haff : ∀ s ∈ K.simplexes, AffineIndependent ℝ fun (v : ↥s) => position' ↑v) (hface : ∀ s ∈ K.simplexes, ∀ t ∈ K.simplexes, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) : ↑K.support ≃ₜ ↑(K.reposition position' hinj haff hface).support

Preserve barycentric coordinates under a repositioning of a complex.

Equations

• K.repositionHomeomorphAll position' hinj haff hface = K.realizationHomeomorphAll.symm.trans (K.reposition position' hinj haff hface).realizationHomeomorphAll

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.repositionMap (K : PlaneComplex) (position' : K.Vertex → Plane) (hinj : Function.Injective position') (haff : ∀ s ∈ K.simplexes, AffineIndependent ℝ fun (v : ↥s) => position' ↑v) (hface : ∀ s ∈ K.simplexes, ∀ t ∈ K.simplexes, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) : Plane → Plane

The ambient function underlying barycentric repositioning, set to zero off the source support.

Equations

• K.repositionMap position' hinj haff hface x = if hx : x ∈ K.support then ↑((K.repositionHomeomorphAll position' hinj haff hface) ⟨x, hx⟩) else 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.repositionMap_apply_realization (K : PlaneComplex) (position' : K.Vertex → Plane) (hinj : Function.Injective position') (haff : ∀ s ∈ K.simplexes, AffineIndependent ℝ fun (v : ↥s) => position' ↑v) (hface : ∀ s ∈ K.simplexes, ∀ t ∈ K.simplexes, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (x : ↑(GeometricRealization K.Vertex K.simplexes)) : K.repositionMap position' hinj haff hface (K.baryEval ↑x) = (K.reposition position' hinj haff hface).baryEval ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.repositionMap_position (K : PlaneComplex) (position' : K.Vertex → Plane) (hinj : Function.Injective position') (haff : ∀ s ∈ K.simplexes, AffineIndependent ℝ fun (v : ↥s) => position' ↑v) (hface : ∀ s ∈ K.simplexes, ∀ t ∈ K.simplexes, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (v : K.Vertex) (hv : {v} ∈ K.simplexes) : K.repositionMap position' hinj haff hface (K.position v) = position' v

Barycentric repositioning sends every vertex which occurs as a zero-face to its prescribed new position.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.repositionMap_affineOn_face (K : PlaneComplex) (position' : K.Vertex → Plane) (hinj : Function.Injective position') (haff : ∀ s ∈ K.simplexes, AffineIndependent ℝ fun (v : ↥s) => position' ↑v) (hface : ∀ s ∈ K.simplexes, ∀ t ∈ K.simplexes, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) : IsAffineOn (K.repositionMap position' hinj haff hface) (K.cellCarrier s)

Barycentric repositioning is affine on each original face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.repositionMap_isPL (K : PlaneComplex) (position' : K.Vertex → Plane) (hinj : Function.Injective position') (haff : ∀ s ∈ K.simplexes, AffineIndependent ℝ fun (v : ↥s) => position' ↑v) (hface : ∀ s ∈ K.simplexes, ∀ t ∈ K.simplexes, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) : IsPLOn K (K.repositionMap position' hinj haff hface)

Barycentric repositioning is PL on the original complex.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.conePosition (K : PlaneComplex) (c : Plane) : Option K.Vertex → Plane

Vertex positions for the cone on K, with none as the cone vertex.

Equations

• K.conePosition c none = c
• K.conePosition c (some v) = K.position v

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.coneWeights (K : PlaneComplex) (z : K.Vertex → ℝ) : Option K.Vertex → ℝ

The coneWeights declaration.

Equations

• K.coneWeights z none = 0
• K.coneWeights z (some v) = z v

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.coneWeights_none (K : PlaneComplex) (z : K.Vertex → ℝ) : K.coneWeights z none = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.coneWeights_some (K : PlaneComplex) (z : K.Vertex → ℝ) (v : K.Vertex) : K.coneWeights z (some v) = z v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sum_coneWeights (K : PlaneComplex) (z : K.Vertex → ℝ) : ∑ v : Option K.Vertex, K.coneWeights z v = ∑ v : K.Vertex, z v

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.liftFace (K : PlaneComplex) (s : Finset K.Vertex) : Finset (Option K.Vertex)

Lift a base face to the non-cone vertices.

Equations

• K.liftFace s = Finset.map Function.Embedding.some s

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baseFace (K : PlaneComplex) (t : Finset (Option K.Vertex)) : Finset K.Vertex

Remove the cone vertex from a cone face.

Equations

• K.baseFace t = Finset.filterMap id t ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_baseFace (K : PlaneComplex) {t : Finset (Option K.Vertex)} {v : K.Vertex} : v ∈ K.baseFace t ↔ some v ∈ t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baseFace_liftFace (K : PlaneComplex) (s : Finset K.Vertex) : K.baseFace (K.liftFace s) = s

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baseFace_inter (K : PlaneComplex) (t u : Finset (Option K.Vertex)) : K.baseFace (t ∩ u) = K.baseFace t ∩ K.baseFace u

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.position_image_inter (K : PlaneComplex) (s t : Finset K.Vertex) : K.position '' ↑s ∩ K.position '' ↑t = K.position '' ↑(s ∩ t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.conePosition_image_eq_of_not_mem_none (K : PlaneComplex) {c : Plane} {t : Finset (Option K.Vertex)} (ht : none ∉ t) : K.conePosition c '' ↑t = K.position '' ↑(K.baseFace t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.conePosition_image_eq_of_mem_none (K : PlaneComplex) {c : Plane} {t : Finset (Option K.Vertex)} (ht : none ∈ t) : K.conePosition c '' ↑t = insert c (K.position '' ↑(K.baseFace t))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.conePosition_injective (K : PlaneComplex) {c : Plane} (hc : c ∉ Set.range K.position) : Function.Injective (K.conePosition c)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.coneSimplexes (K : PlaneComplex) : Finset (Finset (Option K.Vertex))

All nonempty faces of cones on the faces of K.

Equations

• K.coneSimplexes = K.simplexes.biUnion fun (s : Finset K.Vertex) => {x ∈ (insert none (K.liftFace s)).powerset | x.Nonempty}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_coneSimplexes_iff (K : PlaneComplex) {t : Finset (Option K.Vertex)} : t ∈ K.coneSimplexes ↔ t.Nonempty ∧ ∃ s ∈ K.simplexes, t ⊆ insert none (K.liftFace s)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baseFace_subset_of_subset_cone (K : PlaneComplex) {s : Finset K.Vertex} {t : Finset (Option K.Vertex)} (ht : t ⊆ insert none (K.liftFace s)) : K.baseFace t ⊆ s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baseFace_mem_of_nonempty (K : PlaneComplex) {t : Finset (Option K.Vertex)} (ht : t ∈ K.coneSimplexes) (hne : (K.baseFace t).Nonempty) : K.baseFace t ∈ K.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baseCarrier_subset_support (K : PlaneComplex) {t : Finset (Option K.Vertex)} (ht : t ∈ K.coneSimplexes) : (convexHull ℝ) (K.position '' ↑(K.baseFace t)) ⊆ K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baseCarrier_inter (K : PlaneComplex) {t u : Finset (Option K.Vertex)} (ht : t ∈ K.coneSimplexes) (hu : u ∈ K.coneSimplexes) : (convexHull ℝ) (K.position '' ↑(K.baseFace t)) ∩ (convexHull ℝ) (K.position '' ↑(K.baseFace u)) = (convexHull ℝ) (K.position '' ↑(K.baseFace t ∩ K.baseFace u))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.cone (K : PlaneComplex) (S : Set Plane) (hS : Convex ℝ S) (c : Plane) (hc : c ∈ interior S) (havoid : c ∉ Set.range K.position) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hsupport : K.support = frontier S) : PlaneComplex

Cone a finite one-dimensional complex supported on the frontier of a convex set.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.cone_baryEval_coneWeights (K : PlaneComplex) (S : Set Plane) (hS : Convex ℝ S) (c : Plane) (hc : c ∈ interior S) (havoid : c ∉ Set.range K.position) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hsupport : K.support = frontier S) (z : K.Vertex → ℝ) : (K.cone S hS c hc havoid hgraph hsupport).baryEval (K.coneWeights z) = K.baryEval z

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.cone_support_eq (K : PlaneComplex) (S : Set Plane) (hS : Convex ℝ S) (hcompact : IsCompact S) (c : Plane) (hc : c ∈ interior S) (havoid : c ∉ Set.range K.position) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hsupport : K.support = frontier S) (hfrontier : (frontier S).Nonempty) : (K.cone S hS c hc havoid hgraph hsupport).support = S