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 _ _