English
The union over all k of cylinder (update x n k) (n+1) equals cylinder x n.
Русский
Объединение по всем k цилиндров (update x n k) размерности (n+1) даёт цилиндр x n.
LaTeX
$$$\\bigcup_k \\mathrm{cylinder}(\\mathrm{update}(x,n,k),\\;n+1) = \\mathrm{cylinder}(x,n)$$$
Lean4
theorem iUnion_cylinder_update (x : ∀ n, E n) (n : ℕ) : ⋃ k, cylinder (update x n k) (n + 1) = cylinder x n :=
by
ext y
simp only [mem_cylinder_iff, mem_iUnion]
constructor
· rintro ⟨k, hk⟩ i hi
simpa [hi.ne] using hk i (Nat.lt_succ_of_lt hi)
· intro H
refine ⟨y n, fun i hi => ?_⟩
rcases Nat.lt_succ_iff_lt_or_eq.1 hi with (h'i | rfl)
· simp [H i h'i, h'i.ne]
· simp