Theorems · Definition · combinatorics

Equiv.extendSubtype

{α : Type u_1} →
  {p q : α → Prop} →
    [DecidablePred p] → [DecidablePred q] → [Finite ↑{x | p x}] → { x // p x } ≃ { x // q x } → Equiv.Perm α

If e is an equivalence between two subtypes of a type α, e.extendSubtype is a permutation of α acting like e on the subtypes and doing something arbitrary outside. Note that when p = q, Equiv.Perm.subtypeCongr e (Equiv.refl _) can be used instead.

Defined in

Mathlib.Logic.Equiv.Fintype

Cited by

7 results in Mathlib

Foundations

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

Assumes

DecidablePredDecidablePredFinite