comp_inter — Mathlib

English

If g is continuous on t, f is continuous on s, and f^{-1}(t) subset of s, then g∘f is continuous on s.

Русский

Если g непрерывна на t, f непрерывна на s, и \, f^{-1}(t) ⊆ s, то g∘f непрерывна на s.

LaTeX

$$$ (ContinuousOn g t) \land (ContinuousOn f s) \land (f^{-1}(t) \subseteq s) \Rightarrow ContinuousOn (g\circ f) s.$$$

Lean4

theorem comp_inter {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) :
    ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x :=
  hg.comp (hf.mono inter_subset_left) inter_subset_right

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