of_topologicalSpace_le — Mathlib

English

If a topology t is coarser than t′, then any VN bounded set for t is VN bounded for t′.

Русский

Если топология t ⊑ t′, то VN‑ограниченность для t сохраняется для t′.

LaTeX

$$IsVonNBounded 𝕜 s → t ≤ t′ → IsVonNBounded 𝕜 s$$

Lean4

/-- If a topology `t'` is coarser than `t`, then any set `s` that is bounded with respect to
`t` is bounded with respect to `t'`. -/
theorem of_topologicalSpace_le {t t' : TopologicalSpace E} (h : t ≤ t') {s : Set E}
    (hs : @IsVonNBounded 𝕜 E _ _ _ t s) : @IsVonNBounded 𝕜 E _ _ _ t' s := fun _ hV =>
  hs <| (le_iff_nhds t t').mp h 0 hV

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