`BookProof.ChapterF6.mgStep_apply_le` (k : ℕ) (T : α →₀ ℕ) (x y : α) : (mgStep k T x) y ≤ T y + (if y = x then 1 else 0)

Initializing...

`BookProof.ChapterF6.mgStep_apply_le` (k : ℕ) (T : α →₀ ℕ) (x y : α) : (mgStep k T x) y ≤ T y + (if y = x then 1 else 0) · Prove2Me