English
If for all i in I, maps relate s i to t i under f i, then Pi.map f maps I.pi s to I.pi t.
Русский
Если для всех i из I отображения f i переводят s i в t i, то Pi.map f переводит I.pi s в I.pi t.
LaTeX
$$$ ( \forall i \in I, MapsTo (f i) (s i) (t i) ) \Rightarrow Mapsto (\Pi.map f) (I.\pi s) (I.\pi t) $$$
Lean4
theorem eval_image_pi_of_notMem [Decidable (s.pi t).Nonempty] (hi : i ∉ s) :
eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅ := by
classical
ext xᵢ
simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
constructor
· rintro ⟨x, hx, rfl⟩
exact ⟨x, hx⟩
· rintro ⟨x, hx⟩
refine ⟨Function.update x i xᵢ, ?_⟩
simpa +contextual [(ne_of_mem_of_not_mem · hi)]
