English
If e is an equivalence between two subtypes of a finite type α, then e.toCompl is an equivalence between the complements of those subtypes.
Русский
Если e — эквивалентность между двумя подтипами конечного множества α, то e.toCompl — эквивалентность между их дополнениями.
LaTeX
$$$\text{toCompl} : {p q : α \to Prop} \to (\text{Subtype } \{x\mid p x\} \simeq \text{Subtype } \{x\mid q x\}) \to {x\mid \neg p x} \simeq {x\mid \neg q x}$$$
Lean4
/-- If `e` is an equivalence between two subtypes of a finite type `α`, `e.toCompl`
is an equivalence between the complement of those subtypes.
See also `Equiv.compl`, for a computable version when a term of type
`{e' : α ≃ α // ∀ x : {x // p x}, e' x = e x}` is known. -/
noncomputable def toCompl {p q : α → Prop} (e : { x // p x } ≃ { x // q x }) : { x // ¬p x } ≃ { x // ¬q x } :=
by
apply Classical.choice
cases nonempty_fintype α
classical exact Fintype.card_eq.mp <| Fintype.card_compl_eq_card_compl _ _ <| Fintype.card_congr e
