stableUnderGeneralization_range — Mathlib

English

If f is a GeneralizingMap, then the range of f is stable under generalization.

Русский

Если f — обобщающее отображение, то образ f стабилен по обобщению.

LaTeX

$$$\\\\text{GeneralizingMap}(f) \\\\Rightarrow \\\\mathrm{StableUnderGeneralization}(\\\\mathrm{range}(f)).$$$

Lean4

theorem stableUnderGeneralization_range (h : GeneralizingMap f) : StableUnderGeneralization (range f) :=
  @image_univ _ _ f ▸ stableUnderGeneralization_univ.image h

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