Theorems · Theorem

Equiv.subtypeEquivCodomain_symm_apply_ne

∀ {X : Sort u_9} {Y : Sort u_10} [inst : DecidableEq X] {x : X} (f : { x' // x' ≠ x } → Y) (y : Y) (x' : X)
  (h : x' ≠ x), ↑((Equiv.subtypeEquivCodomain f).symm y) x' = f ⟨x', h⟩

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEq