Theorems · Theorem · general topology

UniformFun.gc

∀ (α : Type u_1) (β : Type u_2),
  GaloisConnection (fun 𝓐 => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕

The function UniformFun.filter α β : Filter (β × β) → Filter ((α →ᵤ β) × (α →ᵤ β)) has a lower adjoint l (in the sense of GaloisConnection). The exact definition of l is not interesting; we will only use that it exists (in UniformFun.mono and UniformFun.iInf_eq) and that l (Filter.map (Prod.map f f) 𝓕) = Filter.map (Prod.map ((∘) f) ((∘) f)) (l 𝓕) for each 𝓕 : Filter (γ × γ) and f : γ → α (in UniformFun.comap_eq).

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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