restrict — Mathlib

English

Restrict a bounded continuous function to a subset s ⊆ α to obtain a bounded continuous function on s.

Русский

Ограничение ограниченной непрерывной функции на подмножество s ∈ α даёт ограниченную непрерывную функцию на s.

LaTeX

$$def restrict (f : α →ᵇ β) (s : Set α) : s →ᵇ β$$

Lean4

/-- Restrict a bounded continuous function to a set. -/
def restrict (f : α →ᵇ β) (s : Set α) : s →ᵇ β :=
  f.compContinuous <| (ContinuousMap.id _).restrict s

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