Theorems · Theorem · general topology

UniformOnFun.mono

∀ {α : Type u_1} {γ : Type u_3} ⦃u₁ u₂ : UniformSpace γ⦄,
  u₁ ≤ u₂ → ∀ ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄, 𝔖₂ ⊆ 𝔖₁ → UniformOnFun.uniformSpace α γ 𝔖₁ ≤ UniformOnFun.uniformSpace α γ 𝔖₂

Let u₁, u₂ be two uniform structures on γ and 𝔖₁ 𝔖₂ : Set (Set α). If u₁ ≤ u₂ and 𝔖₂ ⊆ 𝔖₁ then 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂).

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound