enoughInjectives_iff — Mathlib

English

Equivalence preserves the property of having enough injectives in both directions.

Русский

Эквивалентность сохраняет свойство существования достаточно инъективных объектов в обе стороны.

LaTeX

$$$$\\text{EnoughInjectives}(C) \\iff \\text{EnoughInjectives}(D) \\text{ for } C \\simeq D.$$$

Lean4

theorem enoughInjectives_iff (F : C ≌ D) : EnoughInjectives C ↔ EnoughInjectives D :=
  ⟨fun h => h.of_adjunction F.symm.toAdjunction, fun h => h.of_adjunction F.toAdjunction⟩

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