map_comp — Mathlib

English

If i ≤ j ≤ k are indices in Fin 2, then the map from i to k factors as the composition of the maps from i to j and from j to k.

Русский

Если i ≤ j ≤ k — индексы в Fin 2, отображение из i в k расщепляется как композиция отображений из i в j и из j в k.

LaTeX

$$$\forall {i j k : Fin(2)}\ (hij : i \le j) (hjk : j \le k),\ map\ f\ i\ k\ (hij.trans hjk) = map\ f\ i\ j\ hij ≫ map\ f\ j\ k\ hjk$$

Lean4

theorem map_comp {i j k : Fin 2} (hij : i ≤ j) (hjk : j ≤ k) :
    map f i k (hij.trans hjk) = map f i j hij ≫ map f j k hjk :=
  by
  obtain rfl | rfl : i = j ∨ j = k := by cutsat
  · rw [map_id, id_comp]
  · rw [map_id, comp_id]

Похожие утверждения