enoughInjectives — Mathlib

English

The category of types has enough injectives: every object is embedded into an injective object via a suitable construction.

Русский

Категория типов обладает достаточным количеством инъективных объектов: каждый объект внедряется в инъективный посредством подходящей конструции.

LaTeX

$$$$\text{EnoughInjectives}(\text{Type})$$$$

Lean4

instance enoughInjectives : EnoughInjectives (Type u₁) where
  presentation
    X :=
    Nonempty.intro
      { J := WithBot X
        injective := inferInstance
        f := WithBot.some
        mono := by
          rw [mono_iff_injective]
          exact WithBot.coe_injective }

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