isSeparable_preimage — Mathlib

English

If f is an embedding, then the preimage of a separable set is separable.

Русский

Если f — вложение, то прообраз сепарабельного множества сепарабелен.

LaTeX

$$$\\forall f\\, s\\; [\\text{IsEmbedding } f] \\; (\\text{IsSeparable } s) \\Rightarrow \\text{IsSeparable } (f^{-1}[s])$$$

Lean4

protected theorem isSeparable_preimage {f : β → α} [TopologicalSpace β] (hf : IsEmbedding f) {s : Set α}
    (hs : IsSeparable s) : IsSeparable (f ⁻¹' s) :=
  hf.isInducing.isSeparable_preimage hs

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