case mk.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
K₂ : Set α
V₂ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
⊢ ∃ k,
    (IsCompact k.fst ∧ k.snd ∈ 𝓤 β) ∧
      compactConvNhd k.fst k.snd f ⊆
        compactConvNhd (K₁, V₁).fst (K₁, V₁).snd f ∩ compactConvNhd (K₂, V₂).fst (K₂, V₂).snd f
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ ∀ {i j : Set α × Set (β × β)},
    IsCompact i.fst ∧ i.snd ∈ 𝓤 β →
      IsCompact j.fst ∧ j.snd ∈ 𝓤 β →
        ∃ k,
          (IsCompact k.fst ∧ k.snd ∈ 𝓤 β) ∧
            compactConvNhd k.fst k.snd f ⊆ compactConvNhd i.fst i.snd f ∩ compactConvNhd j.fst j.snd f
rintro ⟨K₁, V₁⟩ ⟨K₂, V₂⟩ ⟨hK₁, hV₁⟩ ⟨hK₂, hV₂⟩
no goals
case mk.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
K₂ : Set α
V₂ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
⊢ ∃ k,
    (IsCompact k.fst ∧ k.snd ∈ 𝓤 β) ∧
      compactConvNhd k.fst k.snd f ⊆
        compactConvNhd (K₁, V₁).fst (K₁, V₁).snd f ∩ compactConvNhd (K₂, V₂).fst (K₂, V₂).snd f
exact
  ⟨⟨K₁ ∪ K₂, V₁ ∩ V₂⟩, ⟨hK₁.union hK₂, Filter.inter_mem hV₁ hV₂⟩,
    compactConvNhd_subset_inter f K₁ K₂ V₁ V₂⟩