theorem uniform_inducing.mk' {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (h : ∀ (s : set (α × α)), s ∈ 𝓤 α ↔ ∃ (t : set (β × β)) (H : t ∈ 𝓤 β), ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s) :

theorem uniform_inducing.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {g : β → γ} (hg : uniform_inducing g) {f : α → β} (hf : uniform_inducing f) :

theorem uniform_embedding_subtype_val {α : Type u_1} [uniform_space α] {p : α → Prop} :

theorem uniform_embedding_subtype_coe {α : Type u_1} [uniform_space α] {p : α → Prop} :

theorem uniform_embedding_set_inclusion {α : Type u_1} [uniform_space α] {s t : set α} (hst : s ⊆ t) :

theorem uniform_embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {g : β → γ} (hg : uniform_embedding g) {f : α → β} (hf : uniform_embedding f) :

theorem uniform_embedding_def {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :

theorem uniform_embedding_def' {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :

theorem uniform_inducing.uniform_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (hf : uniform_inducing f) :

theorem uniform_inducing.uniform_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α → β} {g : β → γ} (hg : uniform_inducing g) :

theorem uniform_inducing.inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (h : uniform_inducing f) :

theorem uniform_inducing.prod {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {α' : Type u_3} {β' : Type u_4} [uniform_space α'] [uniform_space β'] {e₁ : α → α'} {e₂ : β → β'} (h₁ : uniform_inducing e₁) (h₂ : uniform_inducing e₂) :

theorem uniform_inducing.dense_inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (h : uniform_inducing f) (hd : dense_range f) :

theorem uniform_embedding.embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (h : uniform_embedding f) :

theorem uniform_embedding.dense_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (h : uniform_embedding f) (hd : dense_range f) :

theorem closure_image_mem_nhds_of_uniform_inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {s : set (α × α)} {e : α → β} (b : β) (he₁ : uniform_inducing e) (he₂ : dense_inducing e) (hs : s ∈ 𝓤 α) :

theorem uniform_embedding_subtype_emb {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (p : α → Prop) {e : α → β} (ue : uniform_embedding e) (de : dense_embedding e) :

theorem uniform_embedding.prod {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {α' : Type u_3} {β' : Type u_4} [uniform_space α'] [uniform_space β'] {e₁ : α → α'} {e₂ : β → β'} (h₁ : uniform_embedding e₁) (h₂ : uniform_embedding e₂) :

theorem is_complete_of_complete_image {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {m : α → β} {s : set α} (hm : uniform_inducing m) (hs : is_complete (m '' s)) :

theorem is_complete_image_iff {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {m : α → β} {s : set α} (hm : uniform_embedding m) :

theorem complete_space_iff_is_complete_range {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (hf : uniform_embedding f) :

theorem complete_space_congr {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {e : α ≃ β} (he : uniform_embedding ⇑e) :

theorem complete_space_coe_iff_is_complete {α : Type u_1} [uniform_space α] {s : set α} :

theorem is_complete.complete_space_coe {α : Type u_1} [uniform_space α] {s : set α} (hs : is_complete s) :

theorem is_closed.complete_space_coe {α : Type u_1} [uniform_space α] [complete_space α] {s : set α} (hs : is_closed s) :

theorem complete_space_extension {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {m : β → α} (hm : uniform_inducing m) (dense : dense_range m) (h : ∀ (f : filter β), cauchy f → (∃ (x : α), filter.map m f ≤ 𝓝 x)) :

theorem totally_bounded_preimage {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} {s : set β} (hf : uniform_embedding f) (hs : totally_bounded s) :

theorem uniform_embedding_comap {α : Type u_1} {β : Type u_2} {f : α → β} [u : uniform_space β] (hf : function.injective f) :

theorem uniformly_extend_exists {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β → α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β → γ} (h_f : uniform_continuous f) [complete_space γ] (a : α) :

theorem uniform_extend_subtype {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] [complete_space γ] {p : α → Prop} {e : α → β} {f : α → γ} {b : β} {s : set α} (hf : uniform_continuous (λ (x : subtype p), f x.val)) (he : uniform_embedding e) (hd : ∀ (x : β), x ∈ closure (set.range e)) (hb : closure (e '' s) ∈ 𝓝 b) (hs : is_closed s) (hp : ∀ (x : α), x ∈ s → p x) :

theorem uniformly_extend_of_ind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β → α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β → γ} (h_f : uniform_continuous f) [separated_space γ] (b : β) :

theorem uniformly_extend_unique {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β → α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β → γ} [separated_space γ] {g : α → γ} (hg : ∀ (b : β), g (e b) = f b) (hc : continuous g) :

theorem uniformly_extend_spec {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β → α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β → γ} (h_f : uniform_continuous f) [separated_space γ] [complete_space γ] (a : α) :

theorem uniform_continuous_uniformly_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β → α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β → γ} (h_f : uniform_continuous f) [separated_space γ] [cγ : complete_space γ] :