continuous_projIcc — Mathlib

English

The extension IccExtend along h is continuous if and only if the base function f on Icc(a,b) is continuous (via a quotient map).

Русский

Расширение IccExtend по h непрерывно тогда и только тогда, когда базовая функция f на Icc(a,b) непрерывна (через факторную карту).

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem continuous_projIcc : Continuous (projIcc a b h) :=
  (continuous_const.max <| continuous_const.min continuous_id).subtype_mk _

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