inl_snd' — Mathlib

English

Variant of IsPullback.of_right with a different left-top origin; uses the same universal property to produce a pullback.

Русский

Вариант IsPullback.of_right с иным левым верхним началом; использует то же самое универсальное свойство для получения пуллбека.

LaTeX

$$$ (s : IsPullback h_{13} v_{11} v_{13} (h_{22})) (t : IsPullback h_{12} v_{12} v_{13} h_{22}) \\Rightarrow IsPullback(h_{11} \\gg h_{13}, v_{11} \\gg h_{21}, v_{12} \\gg v_{22}, h_{23}) $$$

Lean4

theorem inl_snd' {b : BinaryBicone X Y} (h : b.IsBilimit) : IsPullback b.inl (0 : X ⟶ 0) b.snd (0 : 0 ⟶ Y) :=
  by
  refine of_right ?_ (by simp) (of_isBilimit h)
  simp

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