Theorems · Theorem · logic and foundations

Set.sep_or

∀ {α : Type u} {s : Set α} {p q : α → Prop}, {x | x ∈ s ∧ (p x ∨ q x)} = {x | x ∈ s ∧ p x} ∪ {x | x ∈ s ∧ q x}

Defined in

Mathlib.Data.Set.Basic

Cited by

2 results in Mathlib

Foundations

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