instHasInjectiveDimensionLTOfNatNatOfInjective

English

If X is an injective object, then HasInjectiveDimensionLT X 1 holds.

Русский

Если X — инъективный объект, то выполняется HasInjectiveDimensionLT X 1.

LaTeX

$$$\text{Injective}(X) \Rightarrow \text{HasInjectiveDimensionLT}(X,1)$$$

Lean4

instance [Injective X] : HasInjectiveDimensionLT X 1 :=
  by
  letI := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  intro i hi Y e
  obtain _ | i := i
  · simp at hi
  · exact e.eq_zero_of_injective

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