mono_to — Mathlib

English

If HasInitial C and CartesianClosed C, then initial.to B is mono (as an instance).

Русский

Если в C есть начальный объект и C картинианно замкнутая, то initial.to B моно для любого B (инстанс).

LaTeX

$$$[HasInitial\; C]\; (B: C)\; [CartesianClosed\; C] \;:\; Mono(\mathrm{initial.to}\,B)$$

Lean4

instance mono_to [HasInitial C] (B : C) [CartesianClosed C] : Mono (initial.to B) :=
  initial_mono B initialIsInitial

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