stableUnderSpecialization_image — Mathlib

English

If f is a specializing map and s is stable under specialization, then the image f''s is stable under specialization.

Русский

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

LaTeX

$$$\text{SpecializingMap}(f) \Rightarrow (\text{StableUnderSpecialization}(s) \Rightarrow \text{StableUnderSpecialization}(f''s))$$$

Lean4

theorem stableUnderSpecialization_image (hf : SpecializingMap f) {s : Set X} (hs : StableUnderSpecialization s) :
    StableUnderSpecialization (f '' s) :=
  IsLowerSet.image_fibration hf hs

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