Thickness

theorem EGZ.natMassOn_mono_set {α : Type u_1} [Fintype α] (w : α → ℕ) {S T : Set α} (h : S ⊆ T) : natMassOn w S ≤ natMassOn w T

theorem EGZ.slab_mono {p d K T : ℕ} {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} (h : K ≤ T) : slab ξ K ⊆ slab ξ T

theorem EGZ.IsThinAlong.mono_width {p d K T : ℕ} [NeZero p] {w : FpCoord p d → ℕ} {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} {δ : ℝ} (hw : IsThinAlong w ξ K δ) (h : K ≤ T) : IsThinAlong w ξ T δ

theorem EGZ.IsThickAlong.mono_width {p d K T : ℕ} [NeZero p] {w : FpCoord p d → ℕ} {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} {δ : ℝ} (hw : IsThickAlong w ξ T δ) (h : K ≤ T) : IsThickAlong w ξ K δ

theorem EGZ.IsThinAlong.mono_error {p d K : ℕ} [NeZero p] {w : FpCoord p d → ℕ} {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} {δ δ' : ℝ} (hw : IsThinAlong w ξ K δ) (h : δ ≤ δ') : IsThinAlong w ξ K δ'

theorem EGZ.FlagDecomposition.IsCompleteElement.mono_width {p d K T : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {x : Φ.flag.Node} {δ : ℝ} (hw : Φ.IsCompleteElement x T δ) (h : K ≤ T) : Φ.IsCompleteElement x K δ