cylinder_eq_cylinder_union — Mathlib

English

Enlarging the index set by J does not change the cylinder, provided the base is adjusted by the natural restriction map.

Русский

Увеличение множества индексов на J не меняет цилиндр, если основание скорректировать по естественному отображению ограничения.

LaTeX

$$$ \\mathrm{cylinder}(I,S) = \\mathrm{cylinder}(I \\cup J, \\mathrm{restrict}_{2}(\\mathrm{subset\\_union\\_left})^{-1} S). $$$

Lean4

theorem cylinder_eq_cylinder_union [DecidableEq ι] (I : Finset ι) (S : Set (∀ i : I, α i)) (J : Finset ι) :
    cylinder I S = cylinder (I ∪ J) (Finset.restrict₂ Finset.subset_union_left ⁻¹' S) := by ext1 f;
  simp only [mem_cylinder, Finset.restrict_def, Finset.restrict₂_def, mem_preimage]

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