fac — Mathlib

English

For a co-Cartesian φ over f and φ' over f, any ψ with ψ ≫ 𝟙_S = φ' is equal to the induced map IsCocartesian.map p f φ φ'.

Русский

Для ко-Картезианского φ над f и φ' над f, любое ψ с ψ ≫ 𝟙_S = φ' равно отображению IsCocartesian.map p f φ φ'.

LaTeX

$$$\\forall ψ\\ (IsHomLift(p,𝟙 S,ψ))\\ (h: φ \\circ ψ = φ') \\Rightarrow ψ = IsCocartesian.map p f φ φ'$$$

Lean4

@[reassoc (attr := simp)]
theorem fac : φ ≫ IsCocartesian.map p f φ φ' = φ' :=
  (Classical.choose_spec <| IsCocartesian.universal_property (p := p) (f := f) (φ := φ) φ').1.2

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