cylinder_eq_cylinder_of_le_firstDiff

English

If n ≤ firstDiff x y, then cylinder x n = cylinder y n.

Русский

Если n ≤ firstDiff x y, то cylinder x n = cylinder y n.

LaTeX

$$$n \\le \\mathrm{firstDiff}(x,y) \\Rightarrow \\mathrm{cylinder}(x,n)=\\mathrm{cylinder}(y,n)$$$

Lean4

theorem cylinder_eq_cylinder_of_le_firstDiff (x y : ∀ n, E n) {n : ℕ} (hn : n ≤ firstDiff x y) :
    cylinder x n = cylinder y n := by
  rw [← mem_cylinder_iff_eq]
  intro i hi
  exact apply_eq_of_lt_firstDiff (hi.trans_le hn)

Похожие утверждения