GeneralizingMap_iff_stableUnderGeneralization_image

English

A map f is generalizing if and only if for every subset S of X that is generalizing, the image f[S] is generalizing in Y.

Русский

Отображение f является обобщающим тогда и только тогда, когда для любого подмножества S X, сохраняющего обобщение, образ f[S] сохраняет обобщение в Y.

LaTeX

$$$\\\\text{GeneralizingMap}(f) \\\\iff \\\\forall S \\subseteq X, \\\\mathrm{StableUnderGeneralization}(S) \\\\to \\\\mathrm{StableUnderGeneralization}(f[S]).$$$

Lean4

theorem GeneralizingMap_iff_stableUnderGeneralization_image :
    GeneralizingMap f ↔ ∀ s, StableUnderGeneralization s → StableUnderGeneralization (f '' s) :=
  Relation.fibration_iff_isUpperSet_image

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