Theorems · Definition · logic and foundations

Equiv.sumCompl

{α : Type u_9} → (p : α → Prop) → [DecidablePred p] → { a // p a } ⊕ { a // ¬p a } ≃ α

For any predicate p on α, the sum of the two subtypes {a // p a} and its complement {a // ¬ p a} is naturally equivalent to α. See subtypeOrEquiv for sum types over subtypes {x // p x} and {x // q x} that are not necessarily IsCompl p q. See also Equiv.Set.sumCompl for a version on sets.

Defined in

Mathlib.Logic.Equiv.Sum

Cited by

23 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

DecidablePred