iUnion_cylinder_update — Mathlib

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

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