update_preimage_pi — Mathlib

English

Under decidable equality, the preimage of s.pi t under update f i equals t i when the j-th coordinates outside i are unaffected.

Русский

При разрешимой равенству предобраз обновления f i в s.pi t равен t i, если координаты помимо i не меняются.

LaTeX

$$$$ \\mathrm{update}\\ f\\ i^{-1}'(s).\\pi t = t_i. $$$$

Lean4

theorem update_preimage_pi [DecidableEq ι] {f : ∀ i, α i} (hi : i ∈ s) (hf : ∀ j ∈ s, j ≠ i → f j ∈ t j) :
    update f i ⁻¹' s.pi t = t i := by
  ext x
  refine ⟨fun h => ?_, fun hx j hj => ?_⟩
  · convert h i hi
    simp
  · obtain rfl | h := eq_or_ne j i
    · simpa
    · rw [update_of_ne h]
      exact hf j hj h

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