Theorems · Theorem · category theory

DirectLimit.map_def

∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6}
  (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [inst_5 : IsDirectedOrder ι] (ih : (i : ι) → F₁ i → F₂ i)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)) (x : (i : ι) × F₁ i),
  DirectLimit.map f₁ f₂ ih compat ⟦x⟧ = ⟦⟨x.fst, ih x.fst x.snd⟩⟧

Defined in

Mathlib.Order.DirectedInverseSystem

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

PreorderFunLikeDirectedSystemFunLikeDirectedSystemIsDirectedOrder