fac — Mathlib

English

In a suitable diagram with φ strongly Cartesian and two lifts ψ, ψ' of φ, if ψ ≫ φ = φ' = ψ' ≫ φ, then ψ = ψ'.

Русский

В диаграмме с φ сильно-Картезианским и двумя подъёмами ψ, ψ' над φ, если ψ ≫ φ = φ' = ψ' ≫ φ, то ψ = ψ'.

LaTeX

$$$\\text{map\_uniq}(p,f,\\phi, hf', φ')(\\psi) \\; :=\\; \\psi = \\text{map}(p,f,\\phi,hf',φ').$$$

Lean4

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

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