set_biInter_insert_update — Mathlib

English

Similarly, the intersection over insert x t of updates equals the intersection s with the intersection over t of f.

Русский

Аналогично, пересечение через вставку x t от обновления равно пересечению по s с пересечением по t.

LaTeX

$$$$ \\bigcap_{i \\in \\operatorname{insert} x t} \\mathrm{update}(f, x, s)(i) = s \\cap \\bigcap_{i \\in t} f(i) $$$$

Lean4

theorem set_biInter_insert_update {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) :
    ⋂ i ∈ insert x t, @update _ _ _ f x s i = s ∩ ⋂ i ∈ t, f i :=
  iInf_insert_update f hx

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