Theorems · Theorem · category theory

CategoryTheory.Codiscrete.equivFun_symm_apply_map

∀ {X : Type u} {n : ℕ} (f : Fin (n + 1) → X) {X_1 Y : Fin ((Opposite.unop (Opposite.op { len := n })).len + 1)}
  (x : X_1 ⟶ Y), (CategoryTheory.Codiscrete.equivFun.symm f).map x = ({ as := f X_1 }.iso { as := f Y }).hom

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete

Cited by

0 results in Mathlib

Foundations

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