IccExtend — Mathlib

English

Given an order-structured X with a ≤ b and a continuous map on Set.Icc a b, there is a continuous extension to all of α.

Русский

Пусть есть непрерывное отображение из множества Set.Icc(a,b) в β; существует непрерывное вложение в α через IccExtend.

LaTeX

$$IccExtend (f : C(Set.Icc a b, β)) : C(α, β).$$

Lean4

/-- Extend a continuous function `f : C(Set.Icc a b, β)` to a function `f : C(α, β)`. -/
def IccExtend (f : C(Set.Icc a b, β)) : C(α, β) where toFun := Set.IccExtend h f

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