continuous_IccExtend_iff — Mathlib

English

If the family f is continuous in a parameter x and g is continuous at x, then the map a ↦ IccExtend h (f a) (g a) is continuous at x.

Русский

Если семейство f непрерывно по параметру x, а g непрерывна в x, то a ↦ IccExtend h (f a) (g a) непрерывна в x.

LaTeX

$$$\\forall x,\\ (\\text{ContinuousAt } f)\\text{ и } (\\text{ContinuousAt } g)\\Rightarrow \\text{ContinuousAt } (a\\mapsto IccExtend h (f a) (g a)) x.$$$

Lean4

@[simp]
theorem continuous_IccExtend_iff {f : Icc a b → β} : Continuous (IccExtend h f) ↔ Continuous f :=
  isQuotientMap_projIcc.continuous_iff.symm

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