α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : s ⊆ ⋃ (y : α) (_ : y ∈ c), {x | (x, y) ∈ {p | (f p.fst, f p.snd) ∈ t}}
⊢ s ⊆ ⋃ (i : α) (_ : i ∈ c), {a | (f a, f i) ∈ t}
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : s ⊆ ⋃ (y : α) (_ : y ∈ c), {x | (x, y) ∈ {p | (f p.fst, f p.snd) ∈ t}}
⊢ f '' s ⊆ ⋃ (y : β) (_ : y ∈ f '' c), {x | (x, y) ∈ t}
simp [image_subset_iff]
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : ∀ (x : α), x ∈ s → ∃ i, i ∈ c ∧ (f x, f i) ∈ t
⊢ s ⊆ ⋃ (i : α) (_ : i ∈ c), {a | (f a, f i) ∈ t}
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : s ⊆ ⋃ (y : α) (_ : y ∈ c), {x | (x, y) ∈ {p | (f p.fst, f p.snd) ∈ t}}
⊢ s ⊆ ⋃ (i : α) (_ : i ∈ c), {a | (f a, f i) ∈ t}
simp [subset_def] at hct
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : ∀ (x : α), x ∈ s → ∃ i, i ∈ c ∧ (f x, f i) ∈ t
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (i : α) (_ : i ∈ c), {a | (f a, f i) ∈ t}
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : ∀ (x : α), x ∈ s → ∃ i, i ∈ c ∧ (f x, f i) ∈ t
⊢ s ⊆ ⋃ (i : α) (_ : i ∈ c), {a | (f a, f i) ∈ t}
intro x hx
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : ∀ (x : α), x ∈ s → ∃ i, i ∈ c ∧ (f x, f i) ∈ t
x : α
hx : x ∈ s
⊢ ∃ i, i ∈ c ∧ (f x, f i) ∈ t
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : ∀ (x : α), x ∈ s → ∃ i, i ∈ c ∧ (f x, f i) ∈ t
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (i : α) (_ : i ∈ c), {a | (f a, f i) ∈ t}
simp
no goals
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
t : Set (β × β)
ht : t ∈ 𝓤 β
this : {p | (f p.fst, f p.snd) ∈ t} ∈ 𝓤 α
c : Set α
hfc : Set.Finite c
hct : ∀ (x : α), x ∈ s → ∃ i, i ∈ c ∧ (f x, f i) ∈ t
x : α
hx : x ∈ s
⊢ ∃ i, i ∈ c ∧ (f x, f i) ∈ t
exact hct x hx