Theorems · Definition · logic and foundations

Function.Embedding.setValue

{α : Sort u_1} →
  {β : Sort u_2} →
    (f : α ↪ β) → (a : α) → (b : β) → [(a' : α) → Decidable (a' = a)] → [(a' : α) → Decidable (f a' = b)] → α ↪ β

Change the value of an embedding f at one point. If the prescribed image is already occupied by some f a', then swap the values at these two points.

Defined in

Mathlib.Logic.Embedding.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

DecidableDecidable