α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : f ≤ 𝓟 s
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
⊢ IsComplete s
intro f hf hfs
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : f ≤ 𝓟 s
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
rw [le_principal_iff] at hfs
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
⊢ ∃ y, y ∈ m '' s ∧ map m f ≤ 𝓝 y

case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : map m f ≤ 𝓝 (m x)
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
obtain ⟨_, ⟨x, hx, rfl⟩, hyf⟩ : ∃ y ∈ m '' s, map m f ≤ 𝓝 y
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : map m f ≤ 𝓝 (m x)
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
⊢ ∃ y, y ∈ m '' s ∧ map m f ≤ 𝓝 y

case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : map m f ≤ 𝓝 (m x)
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
exact hs (f.map m) (hf.map hm.uniformContinuous) (le_principal_iff.2 (image_mem_map hfs))
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : f ≤ 𝓝 x
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : map m f ≤ 𝓝 (m x)
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
rw [map_le_iff_le_comap, ← nhds_induced, ← hm.inducing.induced] at hyf
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : f ≤ 𝓝 x
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
exact ⟨x, hx, hyf⟩