topologicalSpace_mono — Mathlib

English

Monotonicity of the topological space on UniformConvergenceCLM with respect to 𝔖 inclusion.

Русский

Монотонность топологического пространства UniformConvergenceCLM по включению 𝔖.

LaTeX

$$$$ topologicalSpace\_mono( ) $$$$

Lean4

theorem topologicalSpace_mono [TopologicalSpace F] [IsTopologicalAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) :
    instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂ :=
  by
  letI := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  simp_rw [← uniformity_toTopologicalSpace_eq]
  exact UniformSpace.toTopologicalSpace_mono (uniformSpace_mono σ F h)

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