of_subtype — Mathlib

English

If s is a subset, and the subtype s is separable, then s is separable.

Русский

Если подмножество имеет сепарабельность как подпространство, то оно сепарабельно в исходном пространстве.

LaTeX

$$$IsSeparable(s) \leftarrow IsSeparable\space s$$$

Lean4

theorem of_subtype (s : Set α) [SeparableSpace s] : IsSeparable s := by
  simpa using isSeparable_range (continuous_subtype_val (p := (· ∈ s)))

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