Theorems · Theorem · order theory

Set.update_mem_pi_iff_of_mem

∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} [inst : DecidableEq ι] {a : (i : ι) → α i}
  {i : ι} {b : α i}, a ∈ s.pi t → (Function.update a i b ∈ s.pi t ↔ i ∈ s → b ∈ t i)

Defined in

Mathlib.Data.Set.Prod

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEq