Finite marked-edge fans on intrinsic two-complexes

The relative Radó weld introduces finitely many vertices on the boundary of an intrinsic subcomplex. They must be ordered once on each global abstract edge: ordering independently in the two incident face charts can introduce incompatible auxiliary points. This file supplies that global finite edge order and its consecutive intervals.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking (K : IntrinsicTwoComplex) : Type

A finite set of intrinsic points containing both endpoints of every abstract edge.

• points : Finset K.realization

  The points declaration.

• first_mem (e : K.Edge) : K.edgeFirstPoint e ∈ self.points
• second_mem (e : K.Edge) : K.edgeSecondPoint e ∈ self.points

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.ofFinset (K : IntrinsicTwoComplex) (P : Finset K.realization) : K.EdgeMarking

Enlarge any prescribed finite point set by all abstract edge endpoints.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.subset_points_ofFinset (K : IntrinsicTwoComplex) (P : Finset K.realization) : P ⊆ (ofFinset K P).points

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarks {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : Finset K.realization

The marked points carried by one global abstract edge.

Equations

• M.edgeMarks e = {p ∈ M.points | p ∈ K.faceCarrier ↑e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.mem_edgeMarks_iff {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (p : K.realization) : p ∈ M.edgeMarks e ↔ p ∈ M.points ∧ p ∈ K.faceCarrier ↑e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeFirstPoint_mem_edgeMarks {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : K.edgeFirstPoint e ∈ M.edgeMarks e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeSecondPoint_mem_edgeMarks {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : K.edgeSecondPoint e ∈ M.edgeMarks e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeParameterValue {K : IntrinsicTwoComplex} : K.EdgeMarking → (e : K.Edge) → (p : K.realization) → ℝ

A total real edge parameter. Only its value on the edge carrier is used; totality avoids dependent proof terms in the finite sorting relation.

Equations

• x✝.edgeParameterValue e p = if hp : p ∈ K.faceCarrier ↑e then ↑(K.edgeParameter e p hp) else 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeParameterValue_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) {p : K.realization} (hp : p ∈ K.faceCarrier ↑e) : M.edgeParameterValue e p = ↑(K.edgeParameter e p hp)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeParameterValue_injOn {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : Set.InjOn (M.edgeParameterValue e) (K.faceCarrier ↑e)

The total parameter remains injective when restricted to its intended edge carrier.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.EdgeMark {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : Type

A marked point on one edge.

Equations

• M.EdgeMark e = ↥(M.edgeMarks e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkParameter {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (p : M.EdgeMark e) : ℝ

The edgeMarkParameter declaration.

Equations

• M.edgeMarkParameter e p = M.edgeParameterValue e ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkParameter_injective {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : Function.Injective (M.edgeMarkParameter e)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkLE {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (p q : M.EdgeMark e) : Prop

The edgeMarkLE declaration.

Equations

• M.edgeMarkLE e p q = (M.edgeMarkParameter e p ≤ M.edgeMarkParameter e q)

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkLEDecidable {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : DecidableRel (M.edgeMarkLE e)

Equations

• M.edgeMarkLEDecidable e p q = LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkLEDecidable._aux_1 M e p q

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkLE_total {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : Std.Total (M.edgeMarkLE e)

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkLE_antisymm {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : Std.Antisymm (M.edgeMarkLE e)

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkLE_isTrans {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : IsTrans (M.EdgeMark e) (M.edgeMarkLE e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkList {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : List K.realization

The globally ordered marked points of one abstract edge.

Equations

• M.edgeMarkList e = List.map Subtype.val ((M.edgeMarks e).attach.sort (M.edgeMarkLE e))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.mem_edgeMarkList_iff {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (p : K.realization) : p ∈ M.edgeMarkList e ↔ p ∈ M.edgeMarks e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkList_nodup {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : (M.edgeMarkList e).Nodup

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkList_pairwise_parameter_le {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : List.Pairwise (fun (p q : K.realization) => M.edgeParameterValue e p ≤ M.edgeParameterValue e q) (M.edgeMarkList e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeFirstPoint_ne_edgeSecondPoint {K : IntrinsicTwoComplex} (e : K.Edge) : K.edgeFirstPoint e ≠ K.edgeSecondPoint e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.two_le_edgeMarks_card {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : 2 ≤ (M.edgeMarks e).card

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.two_le_edgeMarkList_length {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : 2 ≤ (M.edgeMarkList e).length

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeParameter_edgeFirstPoint {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : M.edgeParameterValue e (K.edgeFirstPoint e) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeParameter_edgeSecondPoint {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : M.edgeParameterValue e (K.edgeSecondPoint e) = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeParameterValue_mem_Icc {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) {p : K.realization} (hp : p ∈ K.faceCarrier ↑e) : M.edgeParameterValue e p ∈ Set.Icc 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkList_first_parameter {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : M.edgeParameterValue e ((M.edgeMarkList e).get ⟨0, ⋯⟩) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeMarkList_last_parameter {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : M.edgeParameterValue e ((M.edgeMarkList e).get ⟨(M.edgeMarkList e).length - 1, ⋯⟩) = 1

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.EdgeInterval {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) : Type

Consecutive intervals in the globally ordered mark list.

Equations

• M.EdgeInterval e = Fin ((M.edgeMarkList e).length - 1)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeIntervalFirst {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) : K.realization

The edgeIntervalFirst declaration.

Equations

• M.edgeIntervalFirst e j = (M.edgeMarkList e).get ⟨↑j, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeIntervalSecond {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) : K.realization

The edgeIntervalSecond declaration.

Equations

• M.edgeIntervalSecond e j = (M.edgeMarkList e).get ⟨↑j + 1, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeIntervalFirst_mem_edgeMarks {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) : M.edgeIntervalFirst e j ∈ M.edgeMarks e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeIntervalSecond_mem_edgeMarks {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) : M.edgeIntervalSecond e j ∈ M.edgeMarks e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeIntervalFirst_mem_faceCarrier {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) : M.edgeIntervalFirst e j ∈ K.faceCarrier ↑e

The first endpoint of a marked edge interval lies on the underlying geometric edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeIntervalSecond_mem_faceCarrier {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) : M.edgeIntervalSecond e j ∈ K.faceCarrier ↑e

The second endpoint of a marked edge interval lies on the underlying geometric edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeIntervalFirst_ne_second {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) : M.edgeIntervalFirst e j ≠ M.edgeIntervalSecond e j

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeInterval_eq_of_first_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) {a b : M.EdgeInterval e} (h : M.edgeIntervalFirst e a = M.edgeIntervalFirst e b) : a = b

The first marked endpoint determines a consecutive interval uniquely.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeInterval_eq_of_second_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) {a b : M.EdgeInterval e} (h : M.edgeIntervalSecond e a = M.edgeIntervalSecond e b) : a = b

The second marked endpoint determines a consecutive interval uniquely.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeInterval_pair_eq_of_three_common_endpoint {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (a b c : M.EdgeInterval e) (p : K.realization) (ha : p = M.edgeIntervalFirst e a ∨ p = M.edgeIntervalSecond e a) (hb : p = M.edgeIntervalFirst e b ∨ p = M.edgeIntervalSecond e b) (hc : p = M.edgeIntervalFirst e c ∨ p = M.edgeIntervalSecond e c) : a = b ∨ a = c ∨ b = c

Three consecutive intervals on one ordered marked edge which all meet at the same marked point cannot be pairwise distinct.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeInterval_parameter_lt {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) : M.edgeParameterValue e (M.edgeIntervalFirst e j) < M.edgeParameterValue e (M.edgeIntervalSecond e j)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeInterval_eq_of_common_vertex_endpoint {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (a b : M.EdgeInterval e) (v : K.UsedVertex) (hve : ↑v ∈ ↑e) (ha : K.vertexPoint v = M.edgeIntervalFirst e a ∨ K.vertexPoint v = M.edgeIntervalSecond e a) (hb : K.vertexPoint v = M.edgeIntervalFirst e b ∨ K.vertexPoint v = M.edgeIntervalSecond e b) : a = b

At an abstract endpoint of an old edge there is only one incident consecutive interval on that edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeIntervalSecond_parameter_le_first_of_lt {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (a b : M.EdgeInterval e) (hab : ↑a < ↑b) : M.edgeParameterValue e (M.edgeIntervalSecond e a) ≤ M.edgeParameterValue e (M.edgeIntervalFirst e b)

Earlier consecutive intervals on one globally ordered edge end no later than later intervals begin.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeInterval_eq_of_parameter_mem_Ioo {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (a b : M.EdgeInterval e) {z : ℝ} (ha : z ∈ Set.Ioo (M.edgeParameterValue e (M.edgeIntervalFirst e a)) (M.edgeParameterValue e (M.edgeIntervalSecond e a))) (hb : z ∈ Set.Ioo (M.edgeParameterValue e (M.edgeIntervalFirst e b)) (M.edgeParameterValue e (M.edgeIntervalSecond e b))) : a = b

Two open consecutive parameter intervals on the same marked edge can overlap only when their indices agree.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeInterval_endpoints_eq_of_edge_eq_of_parameter_mem_Ioo {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {e d : K.Edge} (hed : e = d) (a : M.EdgeInterval e) (b : M.EdgeInterval d) {z : ℝ} (ha : z ∈ Set.Ioo (M.edgeParameterValue e (M.edgeIntervalFirst e a)) (M.edgeParameterValue e (M.edgeIntervalSecond e a))) (hb : z ∈ Set.Ioo (M.edgeParameterValue d (M.edgeIntervalFirst d b)) (M.edgeParameterValue d (M.edgeIntervalSecond d b))) : M.edgeIntervalFirst e a = M.edgeIntervalFirst d b ∧ M.edgeIntervalSecond e a = M.edgeIntervalSecond d b

Open consecutive intervals on propositionally equal abstract edges have the same two geometric endpoints whenever their parameter interiors overlap.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.exists_edgeInterval_containing {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (p : K.realization) (hp : p ∈ K.faceCarrier ↑e) : ∃ (j : M.EdgeInterval e), M.edgeParameterValue e (M.edgeIntervalFirst e j) ≤ M.edgeParameterValue e p ∧ M.edgeParameterValue e p ≤ M.edgeParameterValue e (M.edgeIntervalSecond e j)

Every point of an abstract edge lies between two consecutive global marks.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.not_edgeMark_parameter_mem_Ioo {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (e : K.Edge) (j : M.EdgeInterval e) {p : K.realization} (hp : p ∈ M.edgeMarks e) : M.edgeParameterValue e p ∉ Set.Ioo (M.edgeParameterValue e (M.edgeIntervalFirst e j)) (M.edgeParameterValue e (M.edgeIntervalSecond e j))

No marked point lies strictly between the endpoints of a consecutive interval.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenter (K : IntrinsicTwoComplex) (t : K.Face) : K.realization

The barycentric center of an intrinsic maximal face.

Equations

• K.faceCenter t = K.faceStandardMap t (K.faceCenterSimplex t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenter_mem_faceCarrier (K : IntrinsicTwoComplex) (t : K.Face) : K.faceCenter t ∈ K.faceCarrier ↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenter_coordinate (K : IntrinsicTwoComplex) (t : K.Face) {v : K.Vertex} (hv : v ∈ ↑t) : ↑(K.faceCenter t) v = 1 / 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenter_ne_vertexPoint (K : IntrinsicTwoComplex) (t : K.Face) (v : K.UsedVertex) : K.faceCenter t ≠ K.vertexPoint v

A barycentric face center is not a vertex point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenter_injective (K : IntrinsicTwoComplex) : Function.Injective K.faceCenter

Distinct maximal intrinsic faces have distinct barycentric centers.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenter_ne_mem_edgeCarrier (K : IntrinsicTwoComplex) (t : K.Face) (e : K.Edge) {p : K.realization} (hp : p ∈ K.faceCarrier ↑e) : K.faceCenter t ≠ p

A barycentric face center cannot lie on any abstract edge of the intrinsic complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edge_eq_of_two_distinct_common_points (K : IntrinsicTwoComplex) (e d : K.Edge) {p q : K.realization} (hpE : p ∈ K.faceCarrier ↑e) (hpD : p ∈ K.faceCarrier ↑d) (hqE : q ∈ K.faceCarrier ↑e) (hqD : q ∈ K.faceCarrier ↑d) (hpq : p ≠ q) : e = d

Two abstract edges which contain the same two distinct intrinsic points are equal.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.intrinsicFaceVertex_add_two_not_mem_faceEdge (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.faceVertex t (i + 2) ∉ ↑(K.faceEdge t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCenter_ne_mem_faceEdge (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {p : K.realization} (hp : p ∈ K.faceCarrier ↑(K.faceEdge t i)) : K.faceCenter t ≠ p

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.FanFace {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : Type

One fan triangle is indexed by an old face, one of its cyclic edges, and one consecutive interval in the global mark order on that edge.

Equations

• M.FanFace = ((t : K.Face) × (i : ZMod 3) × M.EdgeInterval (K.faceEdge t i))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceVertices {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Finset K.realization

The fanFaceVertices declaration.

Equations

• M.fanFaceVertices f = {K.faceCenter f.fst, M.edgeIntervalFirst (K.faceEdge f.fst f.snd.fst) f.snd.snd, M.edgeIntervalSecond (K.faceEdge f.fst f.snd.fst) f.snd.snd}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceVertices_card {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : (M.fanFaceVertices f).card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenter_ne_fanFirst {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f g : M.FanFace) : K.faceCenter f.fst ≠ M.edgeIntervalFirst (K.faceEdge g.fst g.snd.fst) g.snd.snd

A fan center is never one of the marked base vertices of any fan triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenter_ne_fanSecond {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f g : M.FanFace) : K.faceCenter f.fst ≠ M.edgeIntervalSecond (K.faceEdge g.fst g.snd.fst) g.snd.snd

A fan center is never the other marked base vertex of any fan triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.faceCenter_mem_fanFaceVertices_iff {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f g : M.FanFace) : K.faceCenter f.fst ∈ M.fanFaceVertices g ↔ f.fst = g.fst

The center of one fan triangle occurs among the vertices of another exactly when their old parent faces agree.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.eq_fanBase_of_card_two_of_subset_of_center_notMem {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) {e : Finset K.realization} (hecard : e.card = 2) (hef : e ⊆ M.fanFaceVertices f) (hcenter : K.faceCenter f.fst ∉ e) : e = {M.edgeIntervalFirst (K.faceEdge f.fst f.snd.fst) f.snd.snd, M.edgeIntervalSecond (K.faceEdge f.fst f.snd.fst) f.snd.snd}

Removing the center from a two-element subface of a fan triangle leaves exactly its marked base pair.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceVertices_pair_eq_of_three_same_parent_endpoint {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f g h : M.FanFace) (p : K.realization) (hfg : f.fst = g.fst) (hfh : f.fst = h.fst) (hf : p = M.edgeIntervalFirst (K.faceEdge f.fst f.snd.fst) f.snd.snd ∨ p = M.edgeIntervalSecond (K.faceEdge f.fst f.snd.fst) f.snd.snd) (hg : p = M.edgeIntervalFirst (K.faceEdge g.fst g.snd.fst) g.snd.snd ∨ p = M.edgeIntervalSecond (K.faceEdge g.fst g.snd.fst) g.snd.snd) (hh : p = M.edgeIntervalFirst (K.faceEdge h.fst h.snd.fst) h.snd.snd ∨ p = M.edgeIntervalSecond (K.faceEdge h.fst h.snd.fst) h.snd.snd) : M.fanFaceVertices f = M.fanFaceVertices g ∨ M.fanFaceVertices f = M.fanFaceVertices h ∨ M.fanFaceVertices g = M.fanFaceVertices h

Three fan triangles with one old parent which all contain the same radial edge cannot be pairwise distinct. Away from an old vertex all three bases lie on one globally ordered old edge; at an old vertex there are only the two cyclic sides of the parent triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanVertex_mem_faceCarrier {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) {p : K.realization} (hp : p ∈ M.fanFaceVertices f) : p ∈ K.faceCarrier ↑f.fst

Every geometric vertex of a marked fan triangle lies in its parent old face.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenterVertex {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↥(M.fanFaceVertices f)

The distinguished cone-center vertex of a marked fan triangle.

Equations

• M.fanCenterVertex f = ⟨K.faceCenter f.fst, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFirstVertex {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↥(M.fanFaceVertices f)

The first base vertex of a marked fan triangle.

Equations

• M.fanFirstVertex f = ⟨M.edgeIntervalFirst (K.faceEdge f.fst f.snd.fst) f.snd.snd, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanSecondVertex {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↥(M.fanFaceVertices f)

The second base vertex of a marked fan triangle.

Equations

• M.fanSecondVertex f = ⟨M.edgeIntervalSecond (K.faceEdge f.fst f.snd.fst) f.snd.snd, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanVertex_univ {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Finset.univ = {M.fanCenterVertex f, M.fanFirstVertex f, M.fanSecondVertex f}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenterVertex_ne_first {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : M.fanCenterVertex f ≠ M.fanFirstVertex f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenterVertex_ne_second {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : M.fanCenterVertex f ≠ M.fanSecondVertex f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFirstVertex_ne_second {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : M.fanFirstVertex f ≠ M.fanSecondVertex f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f)) → K.realization

The affine barycentric realization of one marked fan triangle inside its parent face.

Equations

• M.fanFaceMap f x = ⟨fun (v : K.Vertex) => ∑ p : ↥(M.fanFaceVertices f), x p * ↑↑p v, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_mem_faceCarrier {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) : M.fanFaceMap f x ∈ K.faceCarrier ↑f.fst

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_vertex {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (p : ↥(M.fanFaceVertices f)) : M.fanFaceMap f (stdSimplex.vertex p) = ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanVertex_val_injective {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Function.Injective fun (p : ↥(M.fanFaceVertices f)) => ↑↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.affineIndependent_fanVertex_val {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : AffineIndependent ℝ fun (p : ↥(M.fanFaceVertices f)) => ↑↑p

The three geometric vertices of a marked fan triangle are affinely independent.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_injective {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Function.Injective (M.fanFaceMap f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.continuous_fanFaceMap {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Continuous (M.fanFaceMap f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.isEmbedding_fanFaceMap {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Topology.IsEmbedding (M.fanFaceMap f)

Each marked fan face is embedded in the intrinsic realization.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanWeights_sum {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) : ↑x (M.fanCenterVertex f) + ↑x (M.fanFirstVertex f) + ↑x (M.fanSecondVertex f) = 1

The three distinguished fan weights sum to one.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBaseSimplexPath {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (r : ↑(Set.Icc 0 1)) : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))

The canonical simplex path along the base of a marked fan triangle.

Equations

• M.fanBaseSimplexPath f r = ⟨(AffineMap.lineMap ⇑(stdSimplex.vertex (M.fanFirstVertex f)) ⇑(stdSimplex.vertex (M.fanSecondVertex f))) ↑r, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBaseSimplexPath_apply_first {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (r : ↑(Set.Icc 0 1)) : (M.fanBaseSimplexPath f r) (M.fanFirstVertex f) = 1 - ↑r

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBaseSimplexPath_apply_second {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (r : ↑(Set.Icc 0 1)) : (M.fanBaseSimplexPath f r) (M.fanSecondVertex f) = ↑r

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBaseSimplexPath_apply_center {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (r : ↑(Set.Icc 0 1)) : (M.fanBaseSimplexPath f r) (M.fanCenterVertex f) = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanSimplexLineMap {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (r : ↑(Set.Icc 0 1)) : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))

The canonical affine segment between two points of one fan simplex.

Equations

• M.fanSimplexLineMap f x y r = ⟨(AffineMap.lineMap ↑x ↑y) ↑r, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_simplexLineMap {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (r : ↑(Set.Icc 0 1)) : ↑(M.fanFaceMap f (M.fanSimplexLineMap f x y r)) = (AffineMap.lineMap ↑(M.fanFaceMap f x) ↑(M.fanFaceMap f y)) ↑r

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBasePath {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↑(Set.Icc 0 1) → K.realization

The geometric path along the base interval of one marked fan triangle.

Equations

• M.fanBasePath f = M.fanFaceMap f ∘ M.fanBaseSimplexPath f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBaseWeights_sum {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (r : ↑(Set.Icc 0 1)) : (M.fanBaseSimplexPath f r) (M.fanFirstVertex f) + (M.fanBaseSimplexPath f r) (M.fanSecondVertex f) = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_mem_baseEdge_of_center_eq_zero {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) = 0) : M.fanFaceMap f x ∈ K.faceCarrier ↑(K.faceEdge f.fst f.snd.fst)

A zero center weight puts a fan point on its declared base edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBasePath_mem_baseEdge {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (r : ↑(Set.Icc 0 1)) : M.fanBasePath f r ∈ K.faceCarrier ↑(K.faceEdge f.fst f.snd.fst)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeParameterValue_fanFaceMap_of_center_eq_zero {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) = 0) : M.edgeParameterValue (K.faceEdge f.fst f.snd.fst) (M.fanFaceMap f x) = x (M.fanFirstVertex f) * M.edgeParameterValue (K.faceEdge f.fst f.snd.fst) ↑(M.fanFirstVertex f) + x (M.fanSecondVertex f) * M.edgeParameterValue (K.faceEdge f.fst f.snd.fst) ↑(M.fanSecondVertex f)

On a fan base, the global edge parameter is the affine combination of its endpoints.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.exists_fanBasePath_eq_of_mem_faceEdge {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (t : K.Face) (i : ZMod 3) {p : K.realization} (hp : p ∈ K.faceCarrier ↑(K.faceEdge t i)) : ∃ (j : M.EdgeInterval (K.faceEdge t i)) (r : ↑(Set.Icc 0 1)), M.fanBasePath ⟨t, ⟨i, j⟩⟩ r = p

Every point of a globally marked edge lies on one consecutive fan base.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneHomeomorph_mem_edge_iff (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {p : K.realization} (hp : p ∈ K.faceCarrier ↑t) : ↑((K.facePlaneHomeomorph t) ⟨p, hp⟩) ∈ standardTriangleCircle.edgeSegment i ↔ p ∈ K.faceCarrier ↑(K.faceEdge t i)

The standard face chart detects membership in each cyclic intrinsic edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneCenter_mem_interior (K : IntrinsicTwoComplex) (t : K.Face) : ↑((K.facePlaneHomeomorph t) ⟨K.faceCenter t, ⋯⟩) ∈ interior standardTrianglePlaneComplex.support

The barycentric center maps to the interior of the standard triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.face_val_eq_lineMap_of_plane_eq (K : IntrinsicTwoComplex) (t : K.Face) (p q : K.ClosedFace t) (r : ℝ) (hplane : ↑((K.facePlaneHomeomorph t) p) = (AffineMap.lineMap ↑((K.facePlaneHomeomorph t) ⟨K.faceCenter t, ⋯⟩) ↑((K.facePlaneHomeomorph t) q)) r) : ↑↑p = (AffineMap.lineMap ↑(K.faceCenter t) ↑↑q) r

A radial segment in the standard face chart pulls back to the same affine segment in intrinsic barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.exists_fanFaceMap_eq_of_mem_faceCarrier {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (t : K.Face) {p : K.realization} (hp : p ∈ K.faceCarrier ↑t) : ∃ (i : ZMod 3) (j : M.EdgeInterval (K.faceEdge t i)) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices ⟨t, ⟨i, j⟩⟩))), M.fanFaceMap ⟨t, ⟨i, j⟩⟩ x = p

The marked fan triangles over one old face cover that entire closed face.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanNormalizedBaseParameter {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) < 1) : ↑(Set.Icc 0 1)

The normalized parameter of the base point obtained by projecting away from the cone center.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanNormalizedBasePoint {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) < 1) : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))

Radial projection of a noncenter fan point to its base simplex.

Equations

• M.fanNormalizedBasePoint f x hxCenter = M.fanBaseSimplexPath f (M.fanNormalizedBaseParameter f x hxCenter)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanNormalizedBasePoint_apply_center {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) < 1) : (M.fanNormalizedBasePoint f x hxCenter) (M.fanCenterVertex f) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanNormalizedBasePoint_apply_second {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) < 1) : (M.fanNormalizedBasePoint f x hxCenter) (M.fanSecondVertex f) = x (M.fanSecondVertex f) / (1 - x (M.fanCenterVertex f))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanNormalizedBasePoint_apply_first {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) < 1) : (M.fanNormalizedBasePoint f x hxCenter) (M.fanFirstVertex f) = x (M.fanFirstVertex f) / (1 - x (M.fanCenterVertex f))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_eq_lineMap_normalizedBase {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) < 1) : ↑(M.fanFaceMap f x) = (AffineMap.lineMap ↑(K.faceCenter f.fst) ↑(M.fanFaceMap f (M.fanNormalizedBasePoint f x hxCenter))) (1 - x (M.fanCenterVertex f))

A noncenter fan point is the affine combination of the cone center and its normalized base projection.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_opposite {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) : ↑(M.fanFaceMap f x) (K.faceVertex f.fst (f.snd.fst + 2)) = x (M.fanCenterVertex f) / 3

The coordinate opposite a fan base is exactly one third of the cone-center weight.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenterWeight_eq_zero_of_mem_baseEdge {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hx : M.fanFaceMap f x ∈ K.faceCarrier ↑(K.faceEdge f.fst f.snd.fst)) : x (M.fanCenterVertex f) = 0

A fan point lies on its declared base edge only if its cone-center weight vanishes.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_faceVertex_lower_bound {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (i : ZMod 3) : x (M.fanCenterVertex f) / 3 ≤ ↑(M.fanFaceMap f x) (K.faceVertex f.fst i)

The center contribution is a lower bound for every parent-face barycentric coordinate.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenterWeight_eq_of_faceMap_eq_of_parent_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (t : K.Face) (i j : ZMod 3) (a : M.EdgeInterval (K.faceEdge t i)) (b : M.EdgeInterval (K.faceEdge t j)) {x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices ⟨t, ⟨j, b⟩⟩))} (hxy : M.fanFaceMap ⟨t, ⟨i, a⟩⟩ x = M.fanFaceMap ⟨t, ⟨j, b⟩⟩ y) : x (M.fanCenterVertex ⟨t, ⟨i, a⟩⟩) = y (M.fanCenterVertex ⟨t, ⟨j, b⟩⟩)

Within one old parent face, a common geometric point determines its cone-center weight.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBaseWeights_sum_of_center_eq_zero {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) = 0) : x (M.fanFirstVertex f) + x (M.fanSecondVertex f) = 1

When the cone-center weight vanishes, the two base weights sum to one.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.edgeParameterValue_fanFaceMap_mem_Ioo_of_center_eq_zero {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) = 0) (hxFirst : 0 < x (M.fanFirstVertex f)) (hxSecond : 0 < x (M.fanSecondVertex f)) : M.edgeParameterValue (K.faceEdge f.fst f.snd.fst) (M.fanFaceMap f x) ∈ Set.Ioo (M.edgeParameterValue (K.faceEdge f.fst f.snd.fst) ↑(M.fanFirstVertex f)) (M.edgeParameterValue (K.faceEdge f.fst f.snd.fst) ↑(M.fanSecondVertex f))

Positive weights at both base vertices put the edge parameter strictly between the two consecutive marked parameters.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_not_mem_points_of_center_zero_of_base_weights_pos {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) = 0) (hxFirst : 0 < x (M.fanFirstVertex f)) (hxSecond : 0 < x (M.fanSecondVertex f)) : M.fanFaceMap f x ∉ M.points

A relative-interior point of a marked fan base is not one of the global marked points.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_mem_edgePath_image_Ioo_of_center_zero_of_base_weights_pos {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) = 0) (hxFirst : 0 < x (M.fanFirstVertex f)) (hxSecond : 0 < x (M.fanSecondVertex f)) : M.fanFaceMap f x ∈ K.edgePath (K.faceEdge f.fst f.snd.fst) '' {r : ↑(Set.Icc 0 1) | 0 < ↑r ∧ ↑r < 1}

A relative-interior point of a fan base lies in the open barycentric carrier of its old abstract edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenterWeight_eq_zero_of_faceMap_eq_of_parent_ne {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} (hfg : f.fst ≠ g.fst) {x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices g))} (hxy : M.fanFaceMap f x = M.fanFaceMap g y) : x (M.fanCenterVertex f) = 0

A point common to fan triangles from distinct old parent faces has zero cone-center weight in the first triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanCenterWeight_eq_zero_of_mem_faceCarrier_of_parent_ne {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (g : K.Face) (hfg : f.fst ≠ g) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxg : M.fanFaceMap f x ∈ K.faceCarrier ↑g) : x (M.fanCenterVertex f) = 0

A fan point lying in a distinct old parent face has zero cone-center weight.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.extendFaceCoordinates_fanFace {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) : extendFaceCoordinates (M.fanFaceVertices f) x = Pi.single (↑(M.fanCenterVertex f)) (x (M.fanCenterVertex f)) + Pi.single (↑(M.fanFirstVertex f)) (x (M.fanFirstVertex f)) + Pi.single (↑(M.fanSecondVertex f)) (x (M.fanSecondVertex f))

Extended coordinates of a marked fan triangle are the sum of its three vertex-weight spikes.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanEndpointData_of_center_eq_zero_of_not_base_weights_pos {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) = 0) (hxNot : ¬(0 < x (M.fanFirstVertex f) ∧ 0 < x (M.fanSecondVertex f))) : ↑(M.fanFaceMap f x) = ↑↑(M.fanFirstVertex f) ∧ extendFaceCoordinates (M.fanFaceVertices f) x = Pi.single (↑(M.fanFirstVertex f)) 1 ∨ ↑(M.fanFaceMap f x) = ↑↑(M.fanSecondVertex f) ∧ extendFaceCoordinates (M.fanFaceVertices f) x = Pi.single (↑(M.fanSecondVertex f)) 1

A zero-center fan point outside the relative interior of its base is one of the declared base vertices, both geometrically and in zero-extended barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanExtendedCoordinates_eq_of_faceMap_eq_of_center_zero_of_base_weights_pos {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} {x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices g))} (hxy : M.fanFaceMap f x = M.fanFaceMap g y) (hxCenter : x (M.fanCenterVertex f) = 0) (hyCenter : y (M.fanCenterVertex g) = 0) (hxFirst : 0 < x (M.fanFirstVertex f)) (hxSecond : 0 < x (M.fanSecondVertex f)) (hyFirst : 0 < y (M.fanFirstVertex g)) (hySecond : 0 < y (M.fanSecondVertex g)) : extendFaceCoordinates (M.fanFaceVertices f) x = extendFaceCoordinates (M.fanFaceVertices g) y

Relative-interior points of fan bases use the same zero-extended coordinates in every fan triangle that contains them. Distinct old edges have disjoint open barycentric carriers, while on one old edge the global mark order determines a unique consecutive interval.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_mem_points_of_center_zero_of_not_base_weights_pos {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) = 0) (hxNot : ¬(0 < x (M.fanFirstVertex f) ∧ 0 < x (M.fanSecondVertex f))) : M.fanFaceMap f x ∈ M.points

A zero-center fan point outside the relative interior of its base is a global marked point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanExtendedCoordinates_eq_of_faceMap_eq_of_center_zero {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} {x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices g))} (hxy : M.fanFaceMap f x = M.fanFaceMap g y) (hxCenter : x (M.fanCenterVertex f) = 0) (hyCenter : y (M.fanCenterVertex g) = 0) : extendFaceCoordinates (M.fanFaceVertices f) x = extendFaceCoordinates (M.fanFaceVertices g) y

Zero-center points in any two marked fan triangles have compatible global barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanNormalizedBaseFaceMap_eq_of_same_parent {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (t : K.Face) (i j : ZMod 3) (a : M.EdgeInterval (K.faceEdge t i)) (b : M.EdgeInterval (K.faceEdge t j)) {x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices ⟨t, ⟨j, b⟩⟩))} (hxy : M.fanFaceMap ⟨t, ⟨i, a⟩⟩ x = M.fanFaceMap ⟨t, ⟨j, b⟩⟩ y) (hxCenter : x (M.fanCenterVertex ⟨t, ⟨i, a⟩⟩) < 1) (hyCenter : y (M.fanCenterVertex ⟨t, ⟨j, b⟩⟩) < 1) : M.fanFaceMap ⟨t, ⟨i, a⟩⟩ (M.fanNormalizedBasePoint ⟨t, ⟨i, a⟩⟩ x hxCenter) = M.fanFaceMap ⟨t, ⟨j, b⟩⟩ (M.fanNormalizedBasePoint ⟨t, ⟨j, b⟩⟩ y hyCenter)

After removing the common center contribution, equal points in one old parent face have equal radial projections to its marked boundary.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.extendFaceCoordinates_eq_center_add_smul_normalizedBase {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))) (hxCenter : x (M.fanCenterVertex f) < 1) : extendFaceCoordinates (M.fanFaceVertices f) x = Pi.single (↑(M.fanCenterVertex f)) (x (M.fanCenterVertex f)) + (1 - x (M.fanCenterVertex f)) • extendFaceCoordinates (M.fanFaceVertices f) (M.fanNormalizedBasePoint f x hxCenter)

Restoring the center weight after radial projection recovers the original zero-extended coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanExtendedCoordinates_eq_of_faceMap_eq_of_same_parent {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (t : K.Face) (i j : ZMod 3) (a : M.EdgeInterval (K.faceEdge t i)) (b : M.EdgeInterval (K.faceEdge t j)) {x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices ⟨t, ⟨i, a⟩⟩))} {y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices ⟨t, ⟨j, b⟩⟩))} (hxy : M.fanFaceMap ⟨t, ⟨i, a⟩⟩ x = M.fanFaceMap ⟨t, ⟨j, b⟩⟩ y) : extendFaceCoordinates (M.fanFaceVertices ⟨t, ⟨i, a⟩⟩) x = extendFaceCoordinates (M.fanFaceVertices ⟨t, ⟨j, b⟩⟩) y

Marked fan triangles in one old parent face assign the same global barycentric coordinates to every common point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanExtendedCoordinates_eq_of_faceMap_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} {x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices g))} (hxy : M.fanFaceMap f x = M.fanFaceMap g y) : extendFaceCoordinates (M.fanFaceVertices f) x = extendFaceCoordinates (M.fanFaceVertices g) y

All marked fan faces use one global barycentric coordinate system on overlaps.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanVertices {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : Finset K.realization

The finite set of every geometric point used as a marked fan vertex.

Equations

• M.fanVertices = Finset.univ.biUnion M.fanFaceVertices

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.FanVertex {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : Type

Geometric vertices occurring in the global marked fan family.

Equations

• M.FanVertex = ↥M.fanVertices

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanVertexEmbedding {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↥(M.fanFaceVertices f) ↪ M.FanVertex

Include the three local vertices of one fan face in the global used-vertex type.

Equations

• M.fanVertexEmbedding f = { toFun := fun (p : ↥(M.fanFaceVertices f)) => ⟨↑p, ⋯⟩, inj' := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFaceVertices {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Finset M.FanVertex

The three vertices of a marked fan face, regarded as global used vertices.

Equations

• M.globalFanFaceVertices f = Finset.map (M.fanVertexEmbedding f) (M.fanFaceVertices f).attach

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.mem_globalFanFaceVertices_iff {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (v : M.FanVertex) : v ∈ M.globalFanFaceVertices f ↔ ↑v ∈ M.fanFaceVertices f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanCenter {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : M.FanVertex

The center vertex of a fan face, included in the global fan-vertex type.

Equations

• M.globalFanCenter f = (M.fanVertexEmbedding f) (M.fanCenterVertex f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFirst {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : M.FanVertex

The first base vertex of a fan face, included in the global fan-vertex type.

Equations

• M.globalFanFirst f = (M.fanVertexEmbedding f) (M.fanFirstVertex f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanSecond {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : M.FanVertex

The second base vertex of a fan face, included in the global fan-vertex type.

Equations

• M.globalFanSecond f = (M.fanVertexEmbedding f) (M.fanSecondVertex f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanCenter_val {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↑(M.globalFanCenter f) = K.faceCenter f.fst

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFirst_val {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↑(M.globalFanFirst f) = M.edgeIntervalFirst (K.faceEdge f.fst f.snd.fst) f.snd.snd

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanSecond_val {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↑(M.globalFanSecond f) = M.edgeIntervalSecond (K.faceEdge f.fst f.snd.fst) f.snd.snd

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFaceVertices_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : M.globalFanFaceVertices f = {M.globalFanCenter f, M.globalFanFirst f, M.globalFanSecond f}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanCenter_ne_first {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f g : M.FanFace) : M.globalFanCenter f ≠ M.globalFanFirst g

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanCenter_ne_second {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f g : M.FanFace) : M.globalFanCenter f ≠ M.globalFanSecond g

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanCenter_eq_iff {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f g : M.FanFace) : M.globalFanCenter f = M.globalFanCenter g ↔ f.fst = g.fst

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.eq_globalFanBase_of_card_two_of_subset_of_center_notMem {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) {e : Finset M.FanVertex} (hecard : e.card = 2) (hef : e ⊆ M.globalFanFaceVertices f) (hcenter : M.globalFanCenter f ∉ e) : e = {M.globalFanFirst f, M.globalFanSecond f}

A two-element subface not containing the fan center is exactly the global base pair.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceVertexEquiv {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↥(M.globalFanFaceVertices f) ≃ ↥(M.fanFaceVertices f)

Relabel global vertices of one face by their underlying intrinsic points.

Equations

• M.fanFaceVertexEquiv f = { toFun := fun (v : ↥(M.globalFanFaceVertices f)) => ⟨↑↑v, ⋯⟩, invFun := fun (p : ↥(M.fanFaceVertices f)) => ⟨⟨↑p, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceVertexEquiv_apply_val {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (v : ↥(M.globalFanFaceVertices f)) : ↑((M.fanFaceVertexEquiv f) v) = ↑↑v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanRelabelSimplex {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f))) : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))

Relabel a simplex on global fan vertices as a simplex on geometric points.

Equations

• M.fanRelabelSimplex f x = stdSimplex.map (⇑(M.fanFaceVertexEquiv f)) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanRelabel_extended_apply {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f))) (v : M.FanVertex) : extendFaceCoordinates (M.fanFaceVertices f) (M.fanRelabelSimplex f x) ↑v = extendFaceCoordinates (M.globalFanFaceVertices f) x v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanRelabel_extended_eq_iff {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} {x : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices g))} : extendFaceCoordinates (M.fanFaceVertices f) (M.fanRelabelSimplex f x) = extendFaceCoordinates (M.fanFaceVertices g) (M.fanRelabelSimplex g y) ↔ extendFaceCoordinates (M.globalFanFaceVertices f) x = extendFaceCoordinates (M.globalFanFaceVertices g) y

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFaceMap {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f)) → K.realization

One marked fan face parametrized by the global used-vertex type.

Equations

• M.globalFanFaceMap f x = M.fanFaceMap f (M.fanRelabelSimplex f x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.continuous_globalFanFaceMap {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Continuous (M.globalFanFaceMap f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.range_globalFanFaceMap {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) : Set.range (M.globalFanFaceMap f) = Set.range (M.fanFaceMap f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFaceMap_mem_faceCarrier {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f))) : M.globalFanFaceMap f x ∈ K.faceCarrier ↑f.fst

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBarycentricAffine {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : (M.FanVertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ

The affine map that evaluates global fan-vertex coordinates in the old intrinsic barycentric space.

Equations

• M.fanBarycentricAffine = (∑ v : M.FanVertex, (LinearMap.proj v).smulRight ↑↑v).toAffineMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanBarycentricAffine_apply {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (z : M.FanVertex → ℝ) : M.fanBarycentricAffine z = fun (k : K.Vertex) => ∑ v : M.FanVertex, z v * ↑↑v k

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFaceMap_val_eq_fanBarycentricAffine {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (f : M.FanFace) (x : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f))) : ↑(M.globalFanFaceMap f x) = M.fanBarycentricAffine (extendFaceCoordinates (M.globalFanFaceVertices f) x)

A globally relabeled fan-face map is affine evaluation at its actual intrinsic vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.fanFaceMap_eq_of_extendedCoordinates_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} {x : ↑(stdSimplex ℝ ↥(M.fanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.fanFaceVertices g))} (hxy : extendFaceCoordinates (M.fanFaceVertices f) x = extendFaceCoordinates (M.fanFaceVertices g) y) : M.fanFaceMap f x = M.fanFaceMap g y

Equal zero-extended geometric-point coordinates give equal marked fan images.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFaceMap_eq_of_extendedCoordinates_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} {x : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices g))} (hxy : extendFaceCoordinates (M.globalFanFaceVertices f) x = extendFaceCoordinates (M.globalFanFaceVertices g) y) : M.globalFanFaceMap f x = M.globalFanFaceMap g y

Equal global fan coordinates are sufficient for equality of geometric images.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanExtendedCoordinates_eq_of_faceMap_eq {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} {x : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices g))} (hxy : M.globalFanFaceMap f x = M.globalFanFaceMap g y) : extendFaceCoordinates (M.globalFanFaceVertices f) x = extendFaceCoordinates (M.globalFanFaceVertices g) y

Equal geometric images of globally relabeled marked fan faces have equal zero-extended barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFaceMap_eq_iff {K : IntrinsicTwoComplex} (M : K.EdgeMarking) {f g : M.FanFace} {x : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices f))} {y : ↑(stdSimplex ℝ ↥(M.globalFanFaceVertices g))} : M.globalFanFaceMap f x = M.globalFanFaceMap g y ↔ extendFaceCoordinates (M.globalFanFaceVertices f) x = extendFaceCoordinates (M.globalFanFaceVertices g) y

Exact face-to-face compatibility of the globally relabeled marked fan family.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.markedFanLocallyFiniteTriangleComplex {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : LocallyFiniteTriangleComplex K.realization

The finite globally compatible marked fan family as an ambient triangle complex in the old intrinsic realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.globalFanFaceFamily_edge_valence {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (hK : K.HasSurfaceEdgeValence) (e : Finset M.FanVertex) (hecard : e.card = 2) : {s ∈ Finset.image M.globalFanFaceVertices Finset.univ | e ⊆ s}.card ≤ 2

The maximal global fan-face family inherits surface edge valence from the old intrinsic complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.markedFanCompactIntrinsic_hasSurfaceEdgeValence {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (hK : K.HasSurfaceEdgeValence) : M.markedFanLocallyFiniteTriangleComplex.compactIntrinsic.HasSurfaceEdgeValence

The compact intrinsic complex underlying the global marked fan has surface edge valence.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.markedFanLocallyFiniteTriangleComplex_support {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : M.markedFanLocallyFiniteTriangleComplex.support = Set.univ

The marked fan family covers the entire old intrinsic realization.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.markedFanGeometricTriangulation {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : GeometricTriangulation K.realization

The finite geometric triangulation of the old realization induced by all global edge marks.

Equations

• M.markedFanGeometricTriangulation = M.markedFanLocallyFiniteTriangleComplex.toGeometricTriangulation ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.markedFanGeometricTriangulation_homeo_apply {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (x : M.markedFanLocallyFiniteTriangleComplex.compactIntrinsic.realization) : M.markedFanGeometricTriangulation.homeo x = M.markedFanLocallyFiniteTriangleComplex.compactEval x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.markedFanHomeomorph {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : M.markedFanLocallyFiniteTriangleComplex.compactIntrinsic.realization ≃ₜ K.realization

The same evaluation homeomorphism with its source stated directly as the compact intrinsic complex, avoiding any projection opacity through GeometricTriangulation.

Equations

• M.markedFanHomeomorph = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.markedFanHomeomorph_apply {K : IntrinsicTwoComplex} (M : K.EdgeMarking) (x : M.markedFanLocallyFiniteTriangleComplex.compactIntrinsic.realization) : M.markedFanHomeomorph x = M.markedFanLocallyFiniteTriangleComplex.compactEval x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeMarking.markedFanSubdivision {K : IntrinsicTwoComplex} (M : K.EdgeMarking) : K.Subdivision

Subdividing every old edge at the global marks and coning the consecutive intervals to the old face centers gives a faithful finite intrinsic subdivision.

Equations

• M.markedFanSubdivision = { refined := M.markedFanLocallyFiniteTriangleComplex.compactIntrinsic, homeo := M.markedFanHomeomorph, affineOnFace := ⋯, subordinate := ⋯ }