Theorems · Theorem · category theory

CategoryTheory.Bicategory.lan.congr_simp

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f f_1 : a ⟶ b) (e_f : f = f_1) (g g_1 : a ⟶ c)
  (e_g : g = g_1) [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g],
  CategoryTheory.Bicategory.lan f g = CategoryTheory.Bicategory.lan f_1 g_1

Defined in: Mathlib.CategoryTheory.Bicategory.Kan.HasKan
Cited by: 0 results in Mathlib
Foundations: Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Bicategory CategoryTheory.Bicategory.HasLeftKanExtension

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Bicategorystatement and proof · cited by 1,587
CategoryTheory.Bicategory.HasLeftKanExtensionstatement and proof · cited by 19
CategoryTheory.Bicategory.lanstatement and proof · cited by 8

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.