English
If two cylinders are equal and one index set is contained in the other, then the base on the smaller index set is the preimage of the base on the larger set under the restriction map.
Русский
Если цилиндры равны и один набор индексов включён в другой, то основание на меньшем наборе индексов получается как прообраз основания на большем наборе через соответствующее ограничение.
LaTeX
$$$ \\text{If } \\mathrm{cylinder}(I,S) = \\mathrm{cylinder}(J,T) \\text{ and } J \\subseteq I, \\text{ then } S = \\mathrm{Finset.restrict}_{2}(hJI)^{-1} T. $$$
Lean4
theorem eq_of_cylinder_eq_of_subset [h_nonempty : Nonempty (∀ i, α i)] {I J : Finset ι} {S : Set (∀ i : I, α i)}
{T : Set (∀ i : J, α i)} (h_eq : cylinder I S = cylinder J T) (hJI : J ⊆ I) : S = Finset.restrict₂ hJI ⁻¹' T :=
by
rw [Set.ext_iff] at h_eq
simp only [mem_cylinder] at h_eq
ext1 f
simp only [mem_preimage]
classical
specialize h_eq fun i ↦ if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i
have h_mem : ∀ j : J, ↑j ∈ I := fun j ↦ hJI j.prop
simpa only [Finset.restrict_def, Finset.coe_mem, dite_true, h_mem] using h_eq
