stableUnderGeneralization_image — Mathlib

English

If f is a GeneralizingMap and S is stable under generalization, then the image f''S is also stable under generalization.

Русский

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

LaTeX

$$$\\\\text{GeneralizingMap}(f) \\\\land \\\\mathrm{StableUnderGeneralization}(S) \\\\Rightarrow \\\\mathrm{StableUnderGeneralization}(f[S]).$$$

Lean4

theorem stableUnderGeneralization_image (hf : GeneralizingMap f) {s : Set X} (hs : StableUnderGeneralization s) :
    StableUnderGeneralization (f '' s) :=
  IsUpperSet.image_fibration hf hs

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