condition_zero — Mathlib

English

Let t be a PushoutCocone f g. Then the component at WalkingSpan.zero equals f followed by the inclusion inl, i.e. ι.app WalkingSpan.zero = f ∘ inl.

Русский

Пусть t — PUSHoutCocone f g. Тогда компонент t.ι.app WalkingSpan.zero равен композиции f с включением inl: t.ι.app WalkingSpan.zero = f ∘ inl.

LaTeX

$$$t.\\iota.app(\\mathrm{WalkingSpan}.zero) = f \\circ t.inl$$$

Lean4

@[simp]
theorem condition_zero (t : PushoutCocone f g) : t.ι.app WalkingSpan.zero = f ≫ t.inl :=
  by
  have w := t.ι.naturality WalkingSpan.Hom.fst
  dsimp at w; simpa using w.symm

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