Theorems · Definition · logic and foundations

Equiv.Set.sumCompl

{α : Type u_3} → (s : Set α) → [DecidablePred fun x => x ∈ s] → ↑s ⊕ ↑sᶜ ≃ α

If s : Set α is a set with decidable membership, then s ⊕ sᶜ is equivalent to α. See also Equiv.sumCompl.

Defined in

Mathlib.Logic.Equiv.Set

Cited by

16 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

DecidablePred