uniformSpace_mono — Mathlib

English

Further monotonicity result for the uniform space under set inclusion.

Русский

Дополнительный факт монотонности uniform space при включении наборов.

LaTeX

$$$$ uniformSpace\_mono(\, ) $$$$

Lean4

theorem uniformSpace_mono [UniformSpace F] [IsUniformAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) :
    instUniformSpace σ F 𝔖₁ ≤ instUniformSpace σ F 𝔖₂ :=
  by
  simp_rw [uniformSpace_eq]
  exact UniformSpace.comap_mono (UniformOnFun.mono (le_refl _) h)

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