mem_cylinder_iff_eq — Mathlib

English

For x,y and n, y ∈ cylinder x n iff cylinder y n = cylinder x n.

Русский

Для последовательностей x,y и числа n верно: y ∈ cylinder(x,n) тогда и только тогда, когда cylinder(y,n)=cylinder(x,n).

LaTeX

$$$y \\in \\mathrm{cylinder}(x,n) \\iff \\mathrm{cylinder}(y,n)=\\mathrm{cylinder}(x,n)$$$

Lean4

theorem mem_cylinder_iff_eq {x y : ∀ n, E n} {n : ℕ} : y ∈ cylinder x n ↔ cylinder y n = cylinder x n :=
  by
  constructor
  · intro hy
    apply Subset.antisymm
    · intro z hz i hi
      rw [← hy i hi]
      exact hz i hi
    · intro z hz i hi
      rw [hy i hi]
      exact hz i hi
  · intro h
    rw [← h]
    exact self_mem_cylinder _ _

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