sumCompl — Mathlib

English

If a decidable predicate exists on a set s, then s ⊕ sᶜ is equivalent to α.

Русский

При существовании разрешимого предиката на множестве s, s ⊕ sᶜ эквивалентно α.

LaTeX

$$s ⊕ (s^c : Set α) ≃ α$$

Lean4

/-- If `s : Set α` is a set with decidable membership, then `s ⊕ sᶜ` is equivalent to `α`. -/
protected def sumCompl {α} (s : Set α) [DecidablePred (· ∈ s)] : s ⊕ (sᶜ : Set α) ≃ α :=
  calc
    s ⊕ (sᶜ : Set α) ≃ ↥(s ∪ sᶜ) := (Equiv.Set.union disjoint_compl_right).symm
    _ ≃ @univ α := (Equiv.setCongr (by simp))
    _ ≃ α := Equiv.Set.univ _

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