instHasLeftResolutionsIdOfContainsIdentities

English

There is an explicit construction of a left resolution for the identity LocalizerMorphism when W₁.ContainsIdentities holds.

Русский

Существует явная конструкция левой резолюции для идентичности LocalizerMorphism при выполнении W₁.ContainsIdentities.

LaTeX

$$$\text{LeftResolutions}(\mathrm{LocalizerMorphism.id\;W_1})$$$

Lean4

instance [W₁.ContainsIdentities] : (LocalizerMorphism.id W₁).HasLeftResolutions := fun X₂ =>
  ⟨LeftResolution.mk (𝟙 X₂) (W₁.id_mem X₂)⟩

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