update_mem_pi_iff_of_mem — Mathlib

English

If a ∈ π s t, then update a i b ∈ π s t is equivalent to i ∈ s → b ∈ t_i.

Русский

Если a ∈ π s t, то обновление a в координате i до b принадлежит π s t тогда и только тогда, когда i ∈ s → b ∈ t_i.

LaTeX

$$$$ \\text{If } a \\in \\pi s t, \\ update\\ a i b \\in \\pi s t \\iff i \\in s \\to b \\in t_i. $$$$

Lean4

theorem update_mem_pi_iff_of_mem [DecidableEq ι] {a : ∀ i, α i} {i : ι} {b : α i} (ha : a ∈ pi s t) :
    update a i b ∈ pi s t ↔ i ∈ s → b ∈ t i :=
  by
  rw [update_mem_pi_iff, and_iff_right]
  exact fun j hj => ha j hj.1

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