preimage — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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