pre_pre — Mathlib

English

If D ⋅ E ⋅ F is a diagram with a limit, then limit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E).

Русский

Если D ⋅ E ⋅ F имеет предел, то limit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E).

LaTeX

$$$\\operatorname{limit.pre} F E \\;\\gg\\; \\operatorname{limit.pre} (E \\cdot F) D = \\operatorname{limit.pre} F (D \\cdot E)$$$

Lean4

@[simp]
theorem pre_pre [h : HasLimit (D ⋙ E ⋙ F)] :
    haveI : HasLimit ((D ⋙ E) ⋙ F) := h
    limit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E) :=
  by
  haveI : HasLimit ((D ⋙ E) ⋙ F) := h
  ext j; erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]; rfl

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