subsingleton — Mathlib

English

From HasInjectiveDimensionLT X n, for any i ≥ n and any Y, Ext^i(Y,X) is a subsingleton.

Русский

Из HasInjectiveDimensionLT X n следует, что для любого i ≥ n и любого Y, Ext^i(Y,X) является множество с одним элементом.

LaTeX

$$$\mathrm{Subsingleton}(\mathrm{Ext}^i(Y,X))$ for all i ≥ n$$

Lean4

theorem subsingleton [hX : HasInjectiveDimensionLT X n] (i : ℕ) (hi : n ≤ i) (Y : C) : Subsingleton (Ext.{w} Y X i) :=
  by
  letI := HasExt.standard C
  have := hX.subsingleton' i hi
  exact Ext.chgUniv.{w, max u v}.symm.subsingleton

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