comp_fract'' — Mathlib

English

If a function f : α → β is continuous on the interval I and f(0) = f(1), then the composition f ∘ fract is continuous on the ambient space.

Русский

Если функция f : α → β непрерывна на отрезке I и f(0) = f(1), то композиция f ∘ fract непрерывна на всей области определения.

LaTeX

$$$\bigl(\mathrm{ContinuousOn}\ f\ I\bigr) \land f(0)=f(1) \Rightarrow \mathrm{Continuous}(f \circ \operatorname{fract}).$$$

Lean4

/-- A special case of `ContinuousOn.comp_fract`. -/
theorem comp_fract'' {f : α → β} (h : ContinuousOn f I) (hf : f 0 = f 1) : Continuous (f ∘ fract) :=
  ContinuousOn.comp_fract (h.comp continuousOn_snd fun _x hx => (mem_prod.mp hx).2) continuous_id fun _ => hf

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