comp — Mathlib

English

If f and g are GeneralizingMap, then their composition g ∘ f is GeneralizingMap.

Русский

Если f и g — обобщающие отображения, то композиция g ∘ f также является обобщающим отображением.

LaTeX

$$$\\\\text{GeneralizingMap}(f) \\\\land \\\\text{GeneralizingMap}(g) \\\\Rightarrow \\\\text{GeneralizingMap}(g\\\\circ f).$$$

Lean4

theorem comp {f : X → Y} {g : Y → Z} (hf : GeneralizingMap f) (hg : GeneralizingMap g) : GeneralizingMap (g ∘ f) :=
  by
  simp only [GeneralizingMap_iff_stableUnderGeneralization_image, Set.image_comp] at *
  exact fun s h ↦ hg _ (hf _ h)

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