compactOpen_le_induced — Mathlib

English

The compact-open topology on C(X,Y) is coarser than the topology induced by restriction to s; in symbols, CO ≤ Induced(restrict s) CO.

Русский

Компактно-открытая топология на C(X,Y) слабее топологии, индуцированной ограничением на s; записывается CO ≤ Induced(restrict s) CO.

LaTeX

$$$(\text{compactOpen}: C(X,Y)) \le \, .\text{induced} (\text{restrict}_s) \; \text{ContinuousMap.compactOpen}$$$

Lean4

theorem compactOpen_le_induced (s : Set X) :
    (ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) ≤ .induced (restrict s) ContinuousMap.compactOpen :=
  (continuous_restrict s).le_induced

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