condition — Mathlib

English

The natural bijection homIso for IsLimit is natural in Z: precomposition on Z' corresponds to precomposition in the target, i.e., the bijection commutes with precomposition by q: Z' ⟶ Z.

Русский

Естественная биекция для гом-изоморфизма IsLimit естественна по Z: предсоставление по q: Z' ⟶ Z согласуется с отображением биекции.

LaTeX

$$$\forall Z,Z',\, q: Z' \to Z,\, k:\, Z \to t.pt,\ (Fork.IsLimit.homIso ht _ (q \circ k)) = q \circ (Fork.IsLimit.homIso ht _ k)$$$

Lean4

@[reassoc]
theorem condition : equalizer.ι f g ≫ f = equalizer.ι f g ≫ g :=
  Fork.condition <| limit.cone <| parallelPair f g

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