Theorems · Theorem · general topology

ContinuousEval.continuous_eval

∀ {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} {inst : FunLike F X Y}
  {inst_1 : TopologicalSpace F} {inst_2 : TopologicalSpace X} {inst_3 : TopologicalSpace Y}
  [self : ContinuousEval F X Y], Continuous fun fx => fx.1 fx.2

Evaluation of a bundled morphism at a point is continuous in both variables.

Defined in

Mathlib.Topology.Hom.ContinuousEval

Cited by

5 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ContinuousEval