comp_inter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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