Monotonicity of the dimension-bounded classes

Kollár's "dim X = n" in [Kol07, Lemma 102, Theorem 103 and Theorem 107] is read throughout the library as "dim X ≤ n" (Triple.HasDimLE), so that disjoint unions and the restriction to a component of the boundary stay in the class; the classes of the stage-n functors — Triple.BOClass n m and MarkedTriple.BMOClass n m — therefore grow with the dimension bound: a triple of dimension ≤ n' has dimension ≤ n for n' ≤ n. These three one-line inclusions place a triple of the smaller class in the larger one; the coherence statements of Hironaka.Resolution.Algebraic.Stage.Coherence and the restriction of the stage-n functor to the stage-n' class (OrderSeqAssignment.restrict) use them.

theorem AlgebraicGeometry.Triple.hasDimLE_mono {k : Type u} [Field k] {n n' : ℕ} (h : n' ≤ n) {T : Triple k} (hT : T.HasDimLE n') : T.HasDimLE n

A triple of dimension ≤ n' has dimension ≤ n for n' ≤ n.

theorem AlgebraicGeometry.Triple.boClass_mono {k : Type u} [Field k] {n n' m : ℕ} (h : n' ≤ n) {T : Triple k} (hT : BOClass n' m T) : BOClass n m T

The class BOClass n' m of [Kol07, Theorem 103] lies in BOClass n m for n' ≤ n.

theorem Hironaka.MarkedTriple.bmoClass_mono {k : Type u} [Field k] {n n' m : ℕ} (h : n' ≤ n) {T : MarkedTriple k} (hT : BMOClass n' m T) : BMOClass n m T

The class BMOClass n' m of [Kol07, Theorem 107] lies in BMOClass n m for n' ≤ n.