English
For any t assigning to each i in s a set of values, the preimage under s.restrict of the product of the t’s equals the Pi-set over s defined by either t i or the universal set, depending on membership in s.
Русский
Для функции t, сопоставляющей каждому i ∈ s множество значений, предобраз в s.restrict от униполной пи-продукции равен пи-набору над s, где для каждого i выбирается t i, если i ∈ s, иначе единичное множество.
LaTeX
$$$\\text{restrict\_preimage} \\,[\\cdot] : s.\\restriction \\to \\, (Set.univ.\\pi t) = \\Pi_{i \\in s} t(i) \\,\\text{with the appropriate piecewise description}.$$$
Lean4
theorem restrict_preimage [DecidablePred (· ∈ s)] (t : (i : s) → Set (π i)) :
s.restrict ⁻¹' (Set.univ.pi t) = Set.pi s (fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ) :=
by
ext x
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, restrict, forall_const, Subtype.forall, mem_coe]
refine ⟨fun h i hi ↦ by simpa [hi] using h i hi, fun h i hi ↦ ?_⟩
convert h i hi
rw [dif_pos hi]
