Skip to content

Instantly share code, notes, and snippets.

@PatrickMassot
Created July 19, 2018 20:25
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save PatrickMassot/beb3b40bec8888b3061d9c410c229467 to your computer and use it in GitHub Desktop.
Save PatrickMassot/beb3b40bec8888b3061d9c410c229467 to your computer and use it in GitHub Desktop.
uniform nonsense
import analysis.topology.uniform_space
universes u v
variables (α : Type u) [uniform_space α]
structure completion_package :=
(space : Type u)
(uniform_structure : uniform_space space)
(completeness : complete_space space)
(separation : separated space)
(map : α → space)
(uniform_continuity : uniform_continuous map)
(lift : ∀ {β : Type u} (f : α → β), space → β)
(lift_uc : ∀ {β : Type u} [uniform_space β] [complete_space β] [separated β] {f : α → β},
uniform_continuous f → uniform_continuous (lift f))
(lift_lifts : ∀ {β : Type u} [uniform_space β] [complete_space β] [separated β] {f : α → β},
uniform_continuous f → f = (lift f) ∘ map)
(lift_unique : ∀ {β : Type u} [uniform_space β] [complete_space β] [separated β]
{f : α → β} (h : uniform_continuous f) {g : space → β},
uniform_continuous g → f = g ∘ map → g = lift f)
variables (pkg pkg' : completion_package α) {α}
def compare (pkg pkg' : completion_package α) : pkg.space → pkg'.space :=
pkg.lift pkg'.map
lemma uniform_continuous_compare :
@uniform_continuous _ _ pkg.uniform_structure pkg'.uniform_structure (compare pkg pkg') :=
begin
haveI := pkg'.uniform_structure,
exact pkg.lift_uc pkg'.uniform_continuity,
sorry
end
open function
lemma compare_iso_aux : left_inverse (compare pkg pkg') (compare pkg' pkg) :=
sorry
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment