case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
⊢ Y ∈ FilterBasis.filter (compactConvergenceFilterBasis f) → ∃ K V _hK _hV, compactConvNhd K V f ⊆ Y

case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
⊢ (∃ K V _hK _hV, compactConvNhd K V f ⊆ Y) → Y ∈ FilterBasis.filter (compactConvergenceFilterBasis f)
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
⊢ Y ∈ FilterBasis.filter (compactConvergenceFilterBasis f) ↔ ∃ K V _hK _hV, compactConvNhd K V f ⊆ Y
constructor
case mp.intro.intro.intro.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
hY : (fun KV => compactConvNhd KV.fst KV.snd f) (K, V) ⊆ Y
⊢ ∃ K V _hK _hV, compactConvNhd K V f ⊆ Y
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
⊢ Y ∈ FilterBasis.filter (compactConvergenceFilterBasis f) → ∃ K V _hK _hV, compactConvNhd K V f ⊆ Y
rintro ⟨X, ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩, hY⟩
no goals
case mp.intro.intro.intro.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
hY : (fun KV => compactConvNhd KV.fst KV.snd f) (K, V) ⊆ Y
⊢ ∃ K V _hK _hV, compactConvNhd K V f ⊆ Y
exact ⟨K, V, hK, hV, hY⟩
case mpr.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact K
hV : V ∈ 𝓤 β
hY : compactConvNhd K V f ⊆ Y
⊢ Y ∈ FilterBasis.filter (compactConvergenceFilterBasis f)
case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
⊢ (∃ K V _hK _hV, compactConvNhd K V f ⊆ Y) → Y ∈ FilterBasis.filter (compactConvergenceFilterBasis f)
rintro ⟨K, V, hK, hV, hY⟩
no goals
case mpr.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f : C(α, β)
Y : Set C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact K
hV : V ∈ 𝓤 β
hY : compactConvNhd K V f ⊆ Y
⊢ Y ∈ FilterBasis.filter (compactConvergenceFilterBasis f)
exact ⟨compactConvNhd K V f, ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩, hY⟩