Theorems · Theorem · logic and foundations

dite_mem

∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α}
  {s : β}, (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Defined in

Mathlib.Logic.Basic

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext, Quot.sound

Assumes

MembershipDecidable