hasWideEqualizers_of_hasLimit_parallelFamily

English

If HasLimit(parallelFamily f) holds for all f, then HasWideEqualizers holds.

Русский

Если для всех f выполняется наличие предела параллельной семьи, то существует широkий эквалайзер.

LaTeX

$$$\forall f,\ HasLimit(parallelFamily f) \Rightarrow HasWideEqualizers C$$

Lean4

/-- If `C` has all limits of diagrams `parallelFamily f`, then it has all wide equalizers -/
theorem hasWideEqualizers_of_hasLimit_parallelFamily
    [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, HasLimit (parallelFamily f)] : HasWideEqualizers.{w} C := fun _ =>
  { has_limit := fun F => hasLimit_of_iso (diagramIsoParallelFamily F).symm }

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