Theorems · Theorem · logic and foundations

FirstOrder.Language.DirectedSystem.map_map

∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] ⦃i j k : ι⦄ (hij : i ≤ j) (hjk : j ≤ k) (x : F i),
  (f j k hjk) ((f i j hij) x) = (f i k ⋯) x

Alias of DirectedSystem.map_map'.

Defined in

Mathlib.ModelTheory.DirectLimit

Cited by

2 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

PreorderFunLikeDirectedSystem