α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ 𝓤 α
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
rw [← hf.comap_uniformity] at ht
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
rcases mem_comap.2 ht with ⟨t', ht', ts⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
rcases totallyBounded_iff_subset.1 (totallyBounded_subset (image_preimage_subset f s) hs) _ ht'
  with ⟨c, cs, hfc, hct⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ f ⁻¹' c), {x | (x, y) ∈ t}
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
refine' ⟨f ⁻¹' c, hfc.preimage (hf.inj.injOn _), fun x h => _⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
this : f x ∈ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
⊢ x ∈ ⋃ (y : α) (_ : y ∈ f ⁻¹' c), {x | (x, y) ∈ t}
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ f ⁻¹' c), {x | (x, y) ∈ t}
have := hct (mem_image_of_mem f h)
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
this : ∃ i, i ∈ c ∧ (f x, i) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
this : f x ∈ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
⊢ x ∈ ⋃ (y : α) (_ : y ∈ f ⁻¹' c), {x | (x, y) ∈ t}
simp at this⊢
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
z : β
zc : z ∈ c
zt : (f x, z) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
this : ∃ i, i ∈ c ∧ (f x, i) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
rcases this with ⟨z, zc, zt⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
y : α
zc : f y ∈ c
zt : (f x, f y) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
z : β
zc : z ∈ c
zt : (f x, z) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
rcases cs zc with ⟨y, -, rfl⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
y : α
zc : f y ∈ c
zt : (f x, f y) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
exact ⟨y, zc, ts zt⟩