instIsContinuousOverForgetOver — Mathlib

English

The forgetful functor from Over X to C is continuous with respect to the topology J.over X and J.

Русский

Забывающая функция Over X → C непрерывна относительно топологий J.over X и J.

LaTeX

$$$\\forall X:\\, (Over.forget X).IsContinuous (J.over X) J$$$

Lean4

instance (X : C) : (Over.forget X).IsContinuous (J.over X) J :=
  Functor.isContinuous_of_coverPreserving (over_forget_compatiblePreserving J X) (over_forget_coverPreserving J X)

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