mem_cylinder_iff_le_firstDiff — Mathlib

English

If x ≠ y, then x ∈ cylinder y i iff i ≤ firstDiff x y.

Русский

Если x ≠ y, то x принадлежит цилиндру вокруг y длины i тогда и только тогда, когда i ≤ firstDiff x y.

LaTeX

$$$\\text{If } x \\neq y:\\; x \\in \\mathrm{cylinder}(y,i) \\iff i \\le \\mathrm{firstDiff}(x,y)$$$

Lean4

theorem mem_cylinder_iff_le_firstDiff {x y : ∀ n, E n} (hne : x ≠ y) (i : ℕ) : x ∈ cylinder y i ↔ i ≤ firstDiff x y :=
  by
  constructor
  · intro h
    by_contra!
    exact apply_firstDiff_ne hne (h _ this)
  · intro hi j hj
    exact apply_eq_of_lt_firstDiff (hj.trans_le hi)

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