theorem exists_scale_add_le_of_mem_minLayer {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {A : Set (𝔓 X)} {p : 𝔓 X} {n : ℕ} (hp : p ∈ A.minLayer n) : ∃ p' ∈ A.minLayer 0, p' ≤ p ∧ 𝔰 p' + ↑n ≤ 𝔰 p

theorem exists_le_add_scale_of_mem_maxLayer {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {A : Set (𝔓 X)} {p : 𝔓 X} {n : ℕ} (hp : p ∈ A.maxLayer n) : ∃ p' ∈ A.maxLayer 0, p ≤ p' ∧ 𝔰 p + ↑n ≤ 𝔰 p'

theorem exists_scale_add_le_of_mem_layersAbove {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {A : Set (𝔓 X)} {p : 𝔓 X} {n : ℕ} (hp : p ∈ A.layersAbove n) : ∃ p' ∈ A.minLayer 0, p' ≤ p ∧ 𝔰 p' + ↑n ≤ 𝔰 p

theorem exists_le_add_scale_of_mem_layersBelow {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {A : Set (𝔓 X)} {p : 𝔓 X} {n : ℕ} (hp : p ∈ A.layersBelow n) : ∃ p' ∈ A.maxLayer 0, p ≤ p' ∧ 𝔰 p + ↑n ≤ 𝔰 p'