pi_update_of_notMem — Mathlib

English

If i ∉ s, then updating i in the Pi-set does not change it.

Русский

Если i не принадлежит s, то обновление i в π-множество не меняет его.

LaTeX

$$$ (s.\pi (\lambda j, t j (\mathrm{update} f i a j))) = s.\pi (\lambda j, t j (f j)) $$$

Lean4

theorem pi_update_of_notMem [DecidableEq ι] (hi : i ∉ s) (f : ∀ j, α j) (a : α i) (t : ∀ j, α j → Set (β j)) :
    (s.pi fun j => t j (update f i a j)) = s.pi fun j => t j (f j) :=
  (pi_congr rfl) fun j hj => by
    rw [update_of_ne]
    exact fun h => hi (h ▸ hj)

Похожие утверждения