isCartesian_of_isStronglyCartesian

English

If a morphism φ is strongly Cartesian over f, then φ is Cartesian over f as well.

Русский

Если морфизм φ является сильно-Картезианским над f, то φ также является Картианским над f.

LaTeX

$$$\\text{IsStronglyCartesian}(p,f,\\phi) \\implies \\text{IsCartesian}(p,f,\\phi).$$$

Lean4

instance isCartesian_of_isStronglyCartesian [p.IsStronglyCartesian f φ] : p.IsCartesian f φ where
  universal_property := fun φ' => universal_property p f φ (𝟙 R) f (by simp) φ'

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