stableUnderSpecialization_range — Mathlib

English

If f is a specializing map, then the range of f is stable under specialization.

Русский

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

LaTeX

$$$\\\\text{SpecializingMap}(f) \\\\Rightarrow \\\\mathrm{StableUnderSpecialization}(\\\\mathrm{range}(f)).$$$

Lean4

theorem stableUnderSpecialization_range (h : SpecializingMap f) : StableUnderSpecialization (range f) :=
  @image_univ _ _ f ▸ stableUnderSpecialization_univ.image h

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