Icc_extend' — Mathlib

English

A useful special case: if f is continuous on Icc(a,b), then IccExtend h f is continuous.

Русский

Полезный частный случай: если f непрерывна на Icc(a,b), то IccExtend h f непрерывна.

LaTeX

$$$\\text{Continuous } f\\Rightarrow \\text{Continuous } (\\IccExtend h f).$$$

Lean4

/-- A useful special case of `Continuous.IccExtend`. -/
@[continuity, fun_prop]
protected theorem Icc_extend' {f : Icc a b → β} (hf : Continuous f) : Continuous (IccExtend h f) :=
  hf.comp continuous_projIcc

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