Theorems · Definition · logic and foundations

Equiv.Set.insert

{α : Type u} → {s : Set α} → [DecidablePred fun x => x ∈ s] → {a : α} → a ∉ s → ↑(insert a s) ≃ ↑s ⊕ PUnit.{u + 1}

If a ∉ s, then insert a s is equivalent to s ⊕ PUnit.

Defined in

Mathlib.Logic.Equiv.Set

Cited by

6 results in Mathlib

Foundations

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

Assumes

DecidablePred