insert — Mathlib

English

If a is not in s, then insert a into s is equivalent to s ⊕ PUnit.

Русский

Если a не принадлежит s, то вставка a в s эквивалентна разложению s на ⊕ PUnit.

LaTeX

$$insert a s ≃ s ⊕ PUnit$$

Lean4

/-- If `a ∉ s`, then `insert a s` is equivalent to `s ⊕ PUnit`. -/
protected def insert {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) :
    (insert a s : Set α) ≃ s ⊕ PUnit.{u + 1} :=
  calc
    (insert a s : Set α) ≃ ↥(s ∪ { a }) := Equiv.setCongr (by simp)
    _ ≃ s ⊕ ({ a } : Set α) := (Equiv.Set.union <| by simpa)
    _ ≃ s ⊕ PUnit.{u + 1} := sumCongr (Equiv.refl _) (Equiv.Set.singleton _)

Похожие утверждения