case intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
hV : V ∈ 𝓤 β
V' : Set (β × β)
h₁ : V' ∈ 𝓤 β
h₂ : V' ○ V' ⊆ V
⊢ ∃ V', V' ∈ 𝓤 β ∧ V' ⊆ V ∧ ∀ (g : C(α, β)), g ∈ compactConvNhd K V' f → compactConvNhd K V' g ⊆ compactConvNhd K V f
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
hV : V ∈ 𝓤 β
⊢ ∃ V', V' ∈ 𝓤 β ∧ V' ⊆ V ∧ ∀ (g : C(α, β)), g ∈ compactConvNhd K V' f → compactConvNhd K V' g ⊆ compactConvNhd K V f
obtain ⟨V', h₁, h₂⟩ := comp_mem_uniformity_sets hV
no goals
case intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
hV : V ∈ 𝓤 β
V' : Set (β × β)
h₁ : V' ∈ 𝓤 β
h₂ : V' ○ V' ⊆ V
⊢ ∃ V', V' ∈ 𝓤 β ∧ V' ⊆ V ∧ ∀ (g : C(α, β)), g ∈ compactConvNhd K V' f → compactConvNhd K V' g ⊆ compactConvNhd K V f
exact
  ⟨V', h₁, Subset.trans (subset_comp_self_of_mem_uniformity h₁) h₂, fun g hg g' hg' =>
    compactConvNhd_mono f h₂ (compactConvNhd_mem_comp f hg hg')⟩