comp_continuous — Mathlib

English

If g: Y → Z is locally constant and f: X → Y is continuous, then g ∘ f is locally constant.

Русский

Если g: Y → Z локально константна, а f: X → Y непрерывна, то g ∘ f локально константна.

LaTeX

$$$IsLocallyConstant g \to Continuous f \to IsLocallyConstant (g \circ f)$$$

Lean4

theorem comp_continuous [TopologicalSpace Y] {g : Y → Z} {f : X → Y} (hg : IsLocallyConstant g) (hf : Continuous f) :
    IsLocallyConstant (g ∘ f) := fun s => by
  rw [Set.preimage_comp]
  exact hf.isOpen_preimage _ (hg _)

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