Theorems · Definition · logic and foundations

subtypeOrEquiv

{α : Type u_1} → (p q : α → Prop) → [DecidablePred p] → Disjoint p q → { x // p x ∨ q x } ≃ { x // p x } ⊕ { x // q x }

A subtype {x // p x ∨ q x} over a disjunction of p q : α → Prop is equivalent to a sum of subtypes {x // p x} ⊕ {x // q x} such that ¬ p x is sent to the right, when Disjoint p q. See also Equiv.sumCompl, for when IsCompl p q.

Defined in

Mathlib.Logic.Embedding.Set

Cited by

6 results in Mathlib

Foundations

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

Assumes

DecidablePred