Theorems · Theorem

Equiv.coe_subtypeEquivCodomain_symm

∀ {X : Sort u_9} {Y : Sort u_10} [inst : DecidableEq X] {x : X} (f : { x' // x' ≠ x } → Y),
  ⇑(Equiv.subtypeEquivCodomain f).symm = fun y => ⟨fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y, ⋯⟩

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEq