English
Projection (evaluation) map sending f to f(i) is locally constant for each i; i-th coordinate projection from a product is locally constant.
Русский
Проекция (оценка) по i-й координате, отправляющая f на f(i), является локально константной; i-й признак проекции из произведения является локально константной.
LaTeX
$$$\\text{eval}_i:\\\\mathrm{LocallyConstant}(\\\\prod_i X_i, X_i) \\to X_i, \\; \\text{defined by } f \\mapsto f(i)\\text{ is locally constant}$$$
Lean4
/-- Evaluation/projection as a locally constant function. -/
@[simps]
def eval {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] (i : ι) [DiscreteTopology (X i)] :
LocallyConstant (Π i, X i) (X i) where
toFun := fun f ↦ f i
isLocallyConstant := (IsLocallyConstant.iff_continuous _).mpr <| continuous_apply i
