isSeparating_separatingFamily — Mathlib

English

If X is a separating family and c has no loop, then the range of separatingFamily c X is a separating family in HomologicalComplex C c.

Русский

Если X является разделяющим семейством и c не имеет петель, то диапазон separatingFamily c X образует разделяющее семейство в категории HomologicalComplex C c.

LaTeX

$$$\text{IsSeparating}(\mathrm{Set.range}(\mathrm{separatingFamily}\,c\,X))$$$

Lean4

theorem isSeparating_separatingFamily : IsSeparating (Set.range (separatingFamily c X)) :=
  by
  intro K L f g h
  ext j
  apply hX
  rintro _ ⟨a, rfl⟩ p
  have H := evalCompCoyonedaCorepresentable c (X a) j
  apply H.homEquiv.symm.injective
  simpa only [H.homEquiv_symm_comp] using h _ ⟨⟨a, j⟩, rfl⟩ (H.homEquiv.symm p)

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