IccExtend — Mathlib

English

The projection map projIcc(a,b,h) from α to the closed interval Icc(a,b) is continuous.

Русский

Проекция projIcc(a,b,h): α → [a,b] непрерывна.

LaTeX

$$$\\text{continuous }(\\text{projIcc } a b h):\\ α\\to Icc(a,b).$$$

Lean4

protected theorem IccExtend (f : γ → Icc a b → β) {la : Filter α} {lb : Filter β} {lc : Filter γ}
    (hf : Tendsto ↿f (lc ×ˢ la.map (projIcc a b h)) lb) : Tendsto (↿(IccExtend h ∘ f)) (lc ×ˢ la) lb :=
  hf.comp <| tendsto_id.prodMap tendsto_map

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