α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ DirectedOn ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1)
    {KV | IsCompact KV.fst ∧ KV.snd ∈ 𝓤 β}
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ HasBasis compactConvergenceUniformity (fun p => IsCompact p.fst ∧ p.snd ∈ 𝓤 β) fun p =>
    {fg | ∀ (x : α), x ∈ p.fst → (↑fg.fst x, ↑fg.snd x) ∈ p.snd}
refine' Filter.hasBasis_biInf_principal _ compactConvNhd_compact_entourage_nonempty
case mk.intro.mk.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
K₂ : Set α
V₂ : Set (β × β)
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
⊢ ∃ z,
    z ∈ {KV | IsCompact KV.fst ∧ KV.snd ∈ 𝓤 β} ∧
      ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1) (K₁, V₁)
          z ∧
        ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1) (K₂, V₂)
          z
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ DirectedOn ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1)
    {KV | IsCompact KV.fst ∧ KV.snd ∈ 𝓤 β}
rintro ⟨K₁, V₁⟩ ⟨hK₁, hV₁⟩ ⟨K₂, V₂⟩ ⟨hK₂, hV₂⟩
case mk.intro.mk.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
K₂ : Set α
V₂ : Set (β × β)
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
⊢ ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1) (K₁, V₁)
      (K₁ ∪ K₂, V₁ ∩ V₂) ∧
    ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1) (K₂, V₂)
      (K₁ ∪ K₂, V₁ ∩ V₂)
case mk.intro.mk.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
K₂ : Set α
V₂ : Set (β × β)
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
⊢ ∃ z,
    z ∈ {KV | IsCompact KV.fst ∧ KV.snd ∈ 𝓤 β} ∧
      ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1) (K₁, V₁)
          z ∧
        ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1) (K₂, V₂)
          z
refine' ⟨⟨K₁ ∪ K₂, V₁ ∩ V₂⟩, ⟨hK₁.union hK₂, Filter.inter_mem hV₁ hV₂⟩, _⟩
case mk.intro.mk.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
K₂ : Set α
V₂ : Set (β × β)
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
⊢ ∀ (x x_1 : C(α, β)),
    (∀ (x_2 : α), x_2 ∈ K₁ ∨ x_2 ∈ K₂ → (↑x x_2, ↑x_1 x_2) ∈ V₁ ∧ (↑x x_2, ↑x_1 x_2) ∈ V₂) →
      ∀ (x_3 : α), (x_3 ∈ K₁ → (↑x x_3, ↑x_1 x_3) ∈ V₁) ∧ (x_3 ∈ K₂ → (↑x x_3, ↑x_1 x_3) ∈ V₂)
case mk.intro.mk.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
K₂ : Set α
V₂ : Set (β × β)
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
⊢ ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1) (K₁, V₁)
      (K₁ ∪ K₂, V₁ ∩ V₂) ∧
    ((fun KV => {fg | ∀ (x : α), x ∈ KV.fst → (↑fg.fst x, ↑fg.snd x) ∈ KV.snd}) ⁻¹'o fun x x_1 => x ≥ x_1) (K₂, V₂)
      (K₁ ∪ K₂, V₁ ∩ V₂)
simp only [le_eq_subset, Prod.forall, setOf_subset_setOf, ge_iff_le, Order.Preimage, ←
  forall_and, mem_inter_iff, mem_union]
no goals
case mk.intro.mk.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
K₂ : Set α
V₂ : Set (β × β)
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
⊢ ∀ (x x_1 : C(α, β)),
    (∀ (x_2 : α), x_2 ∈ K₁ ∨ x_2 ∈ K₂ → (↑x x_2, ↑x_1 x_2) ∈ V₁ ∧ (↑x x_2, ↑x_1 x_2) ∈ V₂) →
      ∀ (x_3 : α), (x_3 ∈ K₁ → (↑x x_3, ↑x_1 x_3) ∈ V₁) ∧ (x_3 ∈ K₂ → (↑x x_3, ↑x_1 x_3) ∈ V₂)
exact fun f g => forall_imp fun x => by tauto
no goals
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ : C(α, β)
K₁ : Set α
V₁ : Set (β × β)
hK₁ : IsCompact (K₁, V₁).fst
hV₁ : (K₁, V₁).snd ∈ 𝓤 β
K₂ : Set α
V₂ : Set (β × β)
hK₂ : IsCompact (K₂, V₂).fst
hV₂ : (K₂, V₂).snd ∈ 𝓤 β
f g : C(α, β)
x : α
⊢ (x ∈ K₁ ∨ x ∈ K₂ → (↑f x, ↑g x) ∈ V₁ ∧ (↑f x, ↑g x) ∈ V₂) →
    (x ∈ K₁ → (↑f x, ↑g x) ∈ V₁) ∧ (x ∈ K₂ → (↑f x, ↑g x) ∈ V₂)
tauto