Labelled piece families on an analytic manifold

Step 3 of the proof of [Kol07, Theorem 107] (item 111) lowers the order of a monomial ideal M(𝓘) = ∏_j 𝓘_{E^j}^{a_j} below m by blowing up intersections of members E^j of the boundary in an order prescribed by the exponents a_j and the order of the index set: at level r one takes the lexicographically smallest r-tuple j₁ < ⋯ < j_r of members with nonempty intersection and maximal exponent sum ≥ m, blows up the intersection, appends the exceptional divisor as the last member with exponent a_{j₁} + ⋯ + a_{j_r} − m, and repeats. The bookkeeping of that procedure is purely combinatorial: which sets of members meet (the nerve), their labels and exponents. It is carried out on the combinatorial state Hironaka.Monomial.MonomialState (a shared module of this library, where the procedure MonomialState.step3, its termination and its postconditions are proved). This file provides the geometric data on an analytic manifold that such a state records.

A PieceFamily N consists of finitely many pieces, closed subsets of N indexed by c < nextComp (the empty set standing for a piece no longer present), each with a label < nextLabel (the position of its boundary member in the order of the members) and an exponent. Its nerve is the set of nonempty sets of pieces with a common point; its state is the corresponding MonomialState, with every data field definitionally the family's. A piece family realises a boundary family F through an order embedding e of its labels into the members of F when each embedded member is the union of the pieces with its label, the members off the range of e are empty (on a relatively compact open set only finitely many members meet the closure), and pieces with the same label are pairwise disjoint: the pieces are then the connected components of the members, which is how the monomial part of this library is indexed (BMO/MonomialPart.lean). The centre of a set S of faces is the union of their loci; for Kollár's choice at level r this is the whole intersection E^{j₁} ∩ ⋯ ∩ E^{j_r} of the chosen members, with all its connected components, as in [Kol07, 111, Step 3].

structure Hironaka.Manifold.BMO.PieceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (N : AnalyticManifold 𝕜 E) : Type u

A labelled piece family on the analytic manifold N: pieces indexed by c < nextComp (closed sets, the empty set for a piece no longer present), each with a label < nextLabel (the position of its boundary member in the order of the members) and an exponent a c. The geometric data behind a combinatorial state Hironaka.Monomial.MonomialState of the monomial procedure of [Kol07, 111, Step 3].

• nextComp : ℕ

  The number of components allocated so far.

• nextLabel : ℕ

  The number of labels (members) allocated so far.

• piece : ℕ → Set N.carrier

  The underlying closed set of a component (∅ for a dead component).

• label : ℕ → ℕ

  The label (member) of a component.

• a : ℕ → ℕ

  The exponent of a component.

• label_lt (c : ℕ) : c < self.nextComp → self.label c < self.nextLabel

  Live components carry live labels.

• isClosed_piece (c : ℕ) : IsClosed (self.piece c)

  Every piece is closed.

def Hironaka.Manifold.BMO.faceCard (S : Finset (Finset ℕ)) : ℕ

The common cardinality of the faces of a centre, its codimension: the maximum of the cardinalities (for a centre of the state all faces have the same label tuple, hence the same cardinality).

Equations

• Hironaka.Manifold.BMO.faceCard S = S.sup Finset.card

Faces and their loci

def Hironaka.Manifold.BMO.PieceFamily.faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (T : Finset ℕ) : Set N.carrier

The locus of a face T: the intersection of its pieces (the whole manifold for T = ∅).

Equations

• Φ.faceSet T = ⋂ c ∈ T, Φ.piece c

theorem Hironaka.Manifold.BMO.PieceFamily.mem_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {T : Finset ℕ} {x : N.carrier} : x ∈ Φ.faceSet T ↔ ∀ c ∈ T, x ∈ Φ.piece c

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.faceSet_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) : Φ.faceSet ∅ = Set.univ

theorem Hironaka.Manifold.BMO.PieceFamily.faceSet_anti {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {T T' : Finset ℕ} (h : T ⊆ T') : Φ.faceSet T' ⊆ Φ.faceSet T

theorem Hironaka.Manifold.BMO.PieceFamily.isClosed_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (T : Finset ℕ) : IsClosed (Φ.faceSet T)

theorem Hironaka.Manifold.BMO.PieceFamily.faceSet_subset_piece {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {T : Finset ℕ} {c : ℕ} (hc : c ∈ T) : Φ.faceSet T ⊆ Φ.piece c

def Hironaka.Manifold.BMO.PieceFamily.total {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (T : Finset ℕ) : ℕ

The exponent sum of a face.

Equations

• Φ.total T = ∑ c ∈ T, Φ.a c

def Hironaka.Manifold.BMO.PieceFamily.labels {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (T : Finset ℕ) : Finset ℕ

The labels of a set of pieces.

Equations

• Φ.labels T = Finset.image Φ.label T

The nerve and the state

noncomputable def Hironaka.Manifold.BMO.PieceFamily.nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) : Finset (Finset ℕ)

The nerve of the family: the nonempty sets of pieces with a common point.

Equations

• Φ.nerve = {T ∈ (Finset.range Φ.nextComp).powerset | T.Nonempty ∧ (Φ.faceSet T).Nonempty}

theorem Hironaka.Manifold.BMO.PieceFamily.mem_nerve_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (T : Finset ℕ) : T ∈ Φ.nerve ↔ T ⊆ Finset.range Φ.nextComp ∧ T.Nonempty ∧ ∃ (x : N.carrier), ∀ c ∈ T, x ∈ Φ.piece c

A set of indices is a face if and only if it consists of indices of pieces, is nonempty, and its pieces have a common point.

theorem Hironaka.Manifold.BMO.PieceFamily.nonempty_of_mem_nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {T : Finset ℕ} (hT : T ∈ Φ.nerve) : T.Nonempty

theorem Hironaka.Manifold.BMO.PieceFamily.lt_nextComp_of_mem_nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {T : Finset ℕ} (hT : T ∈ Φ.nerve) {c : ℕ} (hc : c ∈ T) : c < Φ.nextComp

theorem Hironaka.Manifold.BMO.PieceFamily.faceSet_nonempty_of_mem_nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {T : Finset ℕ} (hT : T ∈ Φ.nerve) : (Φ.faceSet T).Nonempty

theorem Hironaka.Manifold.BMO.PieceFamily.mem_nerve_of_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {T T' : Finset ℕ} (hT : T ∈ Φ.nerve) (hT' : T' ⊆ T) (hne : T'.Nonempty) : T' ∈ Φ.nerve

The nerve is closed under nonempty subsets: the locus of a face is contained in the locus of each of its subsets.

@[reducible, inline]

abbrev Hironaka.Manifold.BMO.PieceFamily.IsValid {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (n m : ℕ) : Prop

The invariants of a combinatorial state (Hironaka.Monomial.MonomialState.Valid) on the family's data: m ≥ 1, faces nonempty and consisting of pieces, labels below nextLabel, the nerve closed under nonempty subsets, faces of cardinality at most n, and pairwise distinct labels on a face.

Equations

• Φ.IsValid n m = Hironaka.Monomial.MonomialState.Valid n m Φ.nextComp Φ.nextLabel Φ.label Φ.nerve

noncomputable def Hironaka.Manifold.BMO.PieceFamily.toState {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (n m : ℕ) (hV : Φ.IsValid n m) : Monomial.MonomialState

The combinatorial state of the family: the state of Hironaka.Monomial.MonomialState with the family's number of pieces and labels, labels, exponents and nerve, each field definitionally the family's.

Equations

• Φ.toState n m hV = Hironaka.Monomial.MonomialState.ofValid n m Φ.nextComp Φ.nextLabel Φ.label Φ.a Φ.nerve hV

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.toState_n {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) : (Φ.toState n m hV).n = n

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.toState_m {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) : (Φ.toState n m hV).m = m

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.toState_nextComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) : (Φ.toState n m hV).nextComp = Φ.nextComp

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.toState_nextLabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) : (Φ.toState n m hV).nextLabel = Φ.nextLabel

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.toState_label {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) : (Φ.toState n m hV).label = Φ.label

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.toState_a {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) : (Φ.toState n m hV).a = Φ.a

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.toState_nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) : (Φ.toState n m hV).nerve = Φ.nerve

theorem Hironaka.Manifold.BMO.PieceFamily.toState_total {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) (T : Finset ℕ) : (Φ.toState n m hV).total T = Φ.total T

theorem Hironaka.Manifold.BMO.PieceFamily.toState_labels {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) (T : Finset ℕ) : (Φ.toState n m hV).labels T = Φ.labels T

noncomputable def Hironaka.Manifold.BMO.PieceFamily.newComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (P : Finset ℕ) : ℕ

The index allocated to the new piece created from the face P of a centre S: the pieces so far, plus the rank of P in S (Hironaka.Monomial.MonomialState.rank).

Equations

• Φ.newComp S P = Φ.nextComp + Hironaka.Monomial.MonomialState.rank S P

theorem Hironaka.Manifold.BMO.PieceFamily.toState_newComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {n m : ℕ} (hV : Φ.IsValid n m) (S : Finset (Finset ℕ)) (P : Finset ℕ) : (Φ.toState n m hV).newComp S P = Φ.newComp S P

The face through a point

noncomputable def Hironaka.Manifold.BMO.PieceFamily.faceAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (x : N.carrier) : Finset ℕ

The face through a point: the pieces containing it.

Equations

• Φ.faceAt x = {c ∈ Finset.range Φ.nextComp | x ∈ Φ.piece c}

theorem Hironaka.Manifold.BMO.PieceFamily.mem_faceAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {x : N.carrier} {c : ℕ} : c ∈ Φ.faceAt x ↔ c < Φ.nextComp ∧ x ∈ Φ.piece c

theorem Hironaka.Manifold.BMO.PieceFamily.faceAt_subset_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (x : N.carrier) : Φ.faceAt x ⊆ Finset.range Φ.nextComp

theorem Hironaka.Manifold.BMO.PieceFamily.mem_faceSet_faceAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (x : N.carrier) : x ∈ Φ.faceSet (Φ.faceAt x)

theorem Hironaka.Manifold.BMO.PieceFamily.faceAt_mem_nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {x : N.carrier} (hx : (Φ.faceAt x).Nonempty) : Φ.faceAt x ∈ Φ.nerve

The face through a point lying on some piece is a face of the nerve.

theorem Hironaka.Manifold.BMO.PieceFamily.subset_faceAt_of_mem_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {T : Finset ℕ} (hT : T ⊆ Finset.range Φ.nextComp) {x : N.carrier} (hx : x ∈ Φ.faceSet T) : T ⊆ Φ.faceAt x

A face whose locus contains x is contained in the face through x.

The centre of a set of faces

def Hironaka.Manifold.BMO.PieceFamily.centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) : Set N.carrier

The centre of a set S of faces: the union of their loci. For Kollár's choice at level r, S consists of all the faces with the lexicographically smallest label tuple j₁ < ⋯ < j_r of maximal exponent sum, so the centre is the whole intersection E^{j₁} ∩ ⋯ ∩ E^{j_r}, with all its connected components, as in [Kol07, 111, Step 3].

Equations

• Φ.centerOf S = ⋃ P ∈ S, Φ.faceSet P

theorem Hironaka.Manifold.BMO.PieceFamily.mem_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {S : Finset (Finset ℕ)} {x : N.carrier} : x ∈ Φ.centerOf S ↔ ∃ P ∈ S, x ∈ Φ.faceSet P

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.centerOf_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) : Φ.centerOf ∅ = ∅

theorem Hironaka.Manifold.BMO.PieceFamily.faceSet_subset_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {S : Finset (Finset ℕ)} {P : Finset ℕ} (hP : P ∈ S) : Φ.faceSet P ⊆ Φ.centerOf S

theorem Hironaka.Manifold.BMO.PieceFamily.isClosed_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) : IsClosed (Φ.centerOf S)

Realising a hypersurface family

structure Hironaka.Manifold.BMO.PieceFamily.Realizes {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (F : Manifold.HypersurfaceFamily N.carrier) (e : Fin Φ.nextLabel ↪o F.ι) : Prop

The family realises the boundary family F through the order embedding e of its labels into the members of F: each embedded member is the union of the pieces with its label, the members off the range of e are empty, and pieces with the same label are pairwise disjoint. The pieces of a realising family are the connected components of the members.

• hyp_eq (ℓ : Fin Φ.nextLabel) : F.hyp (e ℓ) = ⋃ c ∈ {c ∈ Finset.range Φ.nextComp | Φ.label c = ↑ℓ}, Φ.piece c

  An embedded member is the union of the pieces of its label.

• hyp_eq_empty (j : F.ι) : j ∉ Set.range ⇑e → F.hyp j = ∅

  The members off the range of e are empty.

• disjoint (c c' : ℕ) : c < Φ.nextComp → c' < Φ.nextComp → c ≠ c' → Φ.label c = Φ.label c' → Disjoint (Φ.piece c) (Φ.piece c')

  Pieces of one label are pairwise disjoint.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.mem_hyp_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hΦ : Φ.Realizes F e) (ℓ : Fin Φ.nextLabel) (x : N.carrier) : x ∈ F.hyp (e ℓ) ↔ ∃ c < Φ.nextComp, Φ.label c = ↑ℓ ∧ x ∈ Φ.piece c

A point lies on the member with label ℓ if and only if it lies on a piece with that label.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.piece_subset_hyp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hΦ : Φ.Realizes F e) {c : ℕ} (hc : c < Φ.nextComp) : Φ.piece c ⊆ F.hyp (e ⟨Φ.label c, ⋯⟩)

A piece lies in the member of its label.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.eq_of_label_eq_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hΦ : Φ.Realizes F e) {c c' : ℕ} (hc : c < Φ.nextComp) (hc' : c' < Φ.nextComp) (hl : Φ.label c = Φ.label c') {x : N.carrier} (hx : x ∈ Φ.piece c) (hx' : x ∈ Φ.piece c') : c = c'

Through a point passes at most one piece with a given label.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.injOn_label_of_mem_nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hΦ : Φ.Realizes F e) {T : Finset ℕ} (hT : T ∈ Φ.nerve) : Set.InjOn Φ.label ↑T

The labels of the pieces of a face are pairwise distinct: the pieces have a common point.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.card_labels_of_mem_nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hΦ : Φ.Realizes F e) {T : Finset ℕ} (hT : T ∈ Φ.nerve) : (Φ.labels T).card = T.card

A face has as many labels as pieces.