α : Type u_1
β : Type u_2
γ : Type ?u.20997
ι : Type ?u.21000
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕 ↔ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕
α : Type u_1
β : Type u_2
γ : Type ?u.20997
ι : Type ?u.21000
s s' : Set α
x : α
p : Filter ι
g : ι → α
⊢ GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
intro 𝓐 𝓕
α : Type u_1
β : Type u_2
γ : Type ?u.20997
ι : Type ?u.21000
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕 ↔ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕
α : Type u_1
β : Type u_2
γ : Type ?u.20997
ι : Type ?u.21000
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕 ↔ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕
symm
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.20997
ι : Type ?u.21000
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕 ↔ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕
calc
  𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets :=
    by rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
  _ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐 := image_subset_iff
  _ ↔ ∀ U ∈ 𝓕,
        { uv | ∀ x, (uv, x) ∈ { t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U } } ∈
          𝓐 :=
    Iff.rfl
  _ ↔ ∀ U ∈ 𝓕,
        { uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U } ∈
          𝓐 ×ˢ (⊤ : Filter α) :=
    forall₂_congr fun U _hU => mem_prod_top.symm
  _ ↔ lower_adjoint 𝓐 ≤ 𝓕 := Iff.rfl
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.20997
ι : Type ?u.21000
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]