limit_topology — Mathlib

English

If F has a limit, then the topology on the limit object is the initial topology with respect to the projections to each F.obj j; equivalently, it is the infimum of the induced topologies along the limit projections.

Русский

Если у F существует предел, то топология на предельном объекте является начальной топологией по проекциям на каждое F.obj j; эквивалентно, это infimum индуцированных топологий по проекциям предела.

LaTeX

$$$ (\lim F).str = \inf_j (F.obj j).str.induced (\lim.\pi F j) $$$

Lean4

theorem limit_topology [HasLimit F] : (limit F).str = ⨅ j, (F.obj j).str.induced (limit.π F j) :=
  induced_of_isLimit _ (limit.isLimit _)

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