preimage — Mathlib

English

If s is stable under specialization and f is continuous, then the preimage f^{-1}(s) is stable under specialization.

Русский

Если s стабильно по специализации и f непрерывна, то прообраз f^{-1}(s) стабилен по специализации.

LaTeX

$$$StableUnderSpecialization(s) \Rightarrow (\text{Continuous}(f) \Rightarrow StableUnderSpecialization(f^{-1}(s)))$$$

Lean4

theorem preimage {s : Set Y} (hs : StableUnderSpecialization s) (hf : Continuous f) :
    StableUnderSpecialization (f ⁻¹' s) :=
  IsLowerSet.preimage hs hf.specialization_monotone

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