∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a : α i), Function.update f i '' Set.Icc a (f i) = Set.Icc (Function.update f i a) f