instHasCountableLimits — Mathlib

English

Another instance asserting that LightProfinite has countable limits: for any countable diagram F, the limit exists in LightProfinite.

Русский

Ещё одно утверждение о счетных пределах: для любой счетной диаграммы F предел существует в LightProfinite.

LaTeX

$$$\operatorname{HasCountableLimits}(\text{LightProfinite})$$$

Lean4

instance : HasCountableLimits LightProfinite where out _ := { has_limit := fun F ↦ ⟨limitCone F, limitConeIsLimit F⟩ }

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