comp — Mathlib

English

If f: X → Y and g: Y → Z are specializing maps, then their composition g ∘ f is a specializing map.

Русский

Если f: X → Y и g: Y → Z — отображения, сохраняющие специализацию, то композиция g ∘ f сохраняет специализацию.

LaTeX

$$$\\\\text{SpecializingMap}(g\\\\circ f) \\\\Leftarrow \\\\text{SpecializingMap}(f) \\\\land \\\\text{SpecializingMap}(g).$$$

Lean4

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

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