preimage_of_isOpenMap — Mathlib

English

The preimage of a meagre set under a continuous open map is meagre.

Русский

Образ обратной проекции по непрерывному открытию сохраняет мелкость: для любой мелкой множества s в β, f^{-1}(s) мелко.

LaTeX

$$$\\\\forall s \\, (\\\\operatorname{IsMeagre}(s) \\\\Rightarrow \\\\operatorname{IsMeagre}(f^{-1}(s)))$$$

Lean4

/-- The preimage of a meager set under a continuous open map is meager. -/
theorem preimage_of_isOpenMap (hc : Continuous f) (ho : IsOpenMap f) {s : Set β} (h : IsMeagre s) :
    IsMeagre (f ⁻¹' s) :=
  tendsto_residual_of_isOpenMap hc ho h

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