Theorems · Definition · combinatorics

Equiv.toCompl

{α : Type u_1} → {p q : α → Prop} → [Finite ↑{x | p x}] → ↑{x | p x} ≃ ↑{x | q x} → ↑{x | ¬p x} ≃ ↑{x | ¬q x}

If e is an equivalence between two subtypes of a 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.

Defined in

Mathlib.Logic.Equiv.Fintype

Cited by

4 results in Mathlib

Foundations

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

Assumes

Finite