English
For a function f and indices i with a,b in α_i, the image of Icc(a,b) under update f i is Icc(update f i a, update f i b).
Русский
Для функции f и индексов i, a,b ∈ α_i, образ Icc(a,b) под обновлением f i равен Icc(update f i a, update f i b).
LaTeX
$$$$ update f i '' Icc a b = Icc (update f i a) (update f i b) $$$$
Lean4
theorem image_update_Icc (f : ∀ i, α i) (i : ι) (a b : α i) :
update f i '' Icc a b = Icc (update f i a) (update f i b) :=
by
ext x
rw [← Set.pi_univ_Icc]
refine ⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩
· rintro ⟨c, hc, rfl⟩
simpa [update_le_update_iff]
· simpa only [Function.update_self] using h i (mem_univ i)
· ext j
obtain rfl | hij := eq_or_ne i j
· exact Function.update_self ..
· simpa only [Function.update_of_ne hij.symm, le_antisymm_iff] using h j (mem_univ j)
