Theorems · Theorem · general topology

UniformOnFun.gen_mono

∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {S S' : Set α} {V V' : Set (β × β)},
  S' ⊆ S → V ⊆ V' → UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'

UniformOnFun.gen is antitone in the first argument and monotone in the second.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

3 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound