Theorems · Definition

Equiv.Perm.extendDomain

{α' : Type u_9} →
  {β' : Type u_10} → Equiv.Perm α' → {p : β' → Prop} → [DecidablePred p] → α' ≃ Subtype p → Equiv.Perm β'

Extend the domain of e : Equiv.Perm α to one that is over β via f : α → Subtype p, where p : β → Prop, permuting only the b : β that satisfy p b. This can be used to extend the domain across a function f : α → β, keeping everything outside of Set.range f fixed. For this use-case Equiv given by f can be constructed by Equiv.of_leftInverse' or Equiv.of_leftInverse when there is a known inverse, or Equiv.ofInjective in the general case.

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

34 results in Mathlib

Foundations

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

Assumes

DecidablePred