inl_snd' — Mathlib

English

Given a bilimit b of X and Y, the square with arrows b.inl, 0, b.snd, 0 forms a pushout.

Русский

При наличии билилимита b для X и Y квадрат с b.inl, 0, b.snd, 0 образует пушаут.

LaTeX

$$$\operatorname{IsPushout}(b.inl, 0, b.snd, 0)$$$

Lean4

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

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