Theorems · Theorem · order theory

Finset.set_biInter_insert_update

∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] {x : α} {t : Finset α} (f : α → Set β) {s : Set β},
  x ∉ t → ⋂ i ∈ insert x t, Function.update f x s i = s ∩ ⋂ i ∈ t, f i

Defined in

Mathlib.Order.CompleteLattice.Finset

Cited by

0 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq