comp — Mathlib

English

Let f: X → Y be locally constant. Then for any g: Y → Z, the composition g ∘ f: X → Z is locally constant.

Русский

Пусть f: X → Y локально константна. Тогда для любой функции g: Y → Z композиция g ∘ f: X → Z локально константна.

LaTeX

$$$\forall {X Y Z} [TopologicalSpace X] \ {f : X \to Y} (hf : IsLocallyConstant f) (g : Y \to Z), IsLocallyConstant (g \circ f)$$$

Lean4

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

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