instHomIsOverLeftDiscretePUnit — Mathlib

English

If f: X → Y is a morphism in the comma Over S, then the left projection f.left is over S, i.e., HomIsOver f.left S holds with comp_over given by the Over.w construction.

Русский

Если f: X → Y — морфизм в Over S, то левый компонент f.left над S, то есть HomIsOver f.left S, где comp_over задаётся через Over.w f.

LaTeX

$$$[OverClass X S][OverClass Y S]\Rightarrow HomIsOver f.left S$$$

Lean4

instance {S : C} {X Y : Over S} (f : X ⟶ Y) : HomIsOver f.left S where comp_over := Over.w f

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