English
For any α and predicate p, the disjoint union of {a // p a} and its complement {a // ¬ p a} is naturally equivalent to α.
Русский
Для любого множества α и предиката p дисjoint-объединение {a | p(a)} и его дополнения {a | ¬p(a)} естественно эквивалентно α.
LaTeX
$$$${\{ a \mid p(a) \}} \oplus {\{ a \mid \neg p(a) \}} \simeq \alpha.$$$$
Lean4
/-- 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`. -/
def sumCompl {α : Type*} (p : α → Prop) [DecidablePred p] : { a // p a } ⊕ { a // ¬p a } ≃ α
where
toFun := Sum.elim Subtype.val Subtype.val
invFun a := if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩
left_inv := by
rintro (⟨x, hx⟩ | ⟨x, hx⟩) <;> dsimp
· rw [dif_pos]
· rw [dif_neg]
right_inv
a := by
dsimp
split_ifs <;> rfl
