ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>m : γ → β<GOAL>Filter.comap m (f.lift g) = f.lift (Filter.comap m ∘ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>m : β → α<VAR>g : Set β → Filter γ<VAR>hg : Monotone g<GOAL>(Filter.comap m f).lift g = f.lift (g ∘ Set.preimage m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set β → Filter γ<VAR>m : α → β<GOAL>(Filter.map m f).lift g ≤ f.lift (g ∘ Set.image m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set β → Filter γ<VAR>m : α → β<VAR>hg : Monotone g<GOAL>(Filter.map m f).lift g = f.lift (g ∘ Set.image m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Set α → Set β → Filter γ<GOAL>(f.lift fun s => g.lift (h s)) = g.lift fun t => f.lift fun s => h s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>h : Set β → Filter γ<VAR>hg : Monotone g<GOAL>(f.lift g).lift h = f.lift fun s => (g s).lift h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Set α → Filter β<GOAL>(f.lift fun s => f.lift (g s)) ≤ f.lift fun s => g s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Set α → Filter β<VAR>hg₁ : ∀ (s : Set α), Monotone fun t => g s t<VAR>hg₂ : ∀ (t : Set α), Monotone fun s => g s t<GOAL>(f.lift fun s => f.lift (g s)) = f.lift fun s => g s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : Set α → Filter β<VAR>s : Set α<VAR>hg : Monotone g<GOAL>(𝓟 s).lift g = g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder γ<VAR>f : γ → Filter α<VAR>g : γ → Set α → Filter β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun c => (f c).lift (g c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>hm : Monotone g<GOAL>(f.lift g).NeBot ↔ ∀ s ∈ f, (g s).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f.lift fun x => g) = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g h : Set α → Filter β<GOAL>(f.lift fun x => g x ⊓ h x) = f.lift g ⊓ f.lift h
<VAR>α : Type u_1<VAR>f : Filter α<GOAL>f.lift 𝓟 = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<GOAL>(iInf f).lift g ≤ ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<GOAL>(iInf f).lift g = ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hf : Directed (fun x x_1 => x ≥ x_1) f<VAR>hg : Monotone g<GOAL>(iInf f).lift g = ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<VAR>hg' : g Set.univ = ⊤<GOAL>(iInf f).lift g = ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>h : Set α → Set β<GOAL>⊤.lift' h = 𝓟 (h Set.univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>t : Set α<VAR>ht : t ∈ f<GOAL>h t ∈ f.lift' h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>m : γ → β<VAR>l : Filter γ<GOAL>Filter.Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hf : f.HasBasis p s<VAR>hh : Monotone h<GOAL>(f.lift' h).HasBasis p (h ∘ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>hh : Monotone h<VAR>s : Set β<GOAL>s ∈ f.lift' h ↔ ∃ t ∈ f, h t ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>hh : Monotone h<VAR>p : β → Prop<GOAL>(∀ᶠ (y : β) in f.lift' h, p y) ↔ ∃ t ∈ f, ∀ y ∈ h t, p y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>hh : Monotone h<GOAL>⋂₀ {s | s ∈ f.lift' h} = ⋂ s ∈ f, h s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Set β<VAR>h : Filter β<VAR>s : Set α<VAR>hs : s ∈ f<VAR>hg : 𝓟 (g s) ≤ h<GOAL>f.lift' g ≤ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f₁ f₂ : Filter α<VAR>h₁ h₂ : Set α → Set β<VAR>hf : f₁ ≤ f₂<VAR>hh : h₁ ≤ h₂<GOAL>f₁.lift' h₁ ≤ f₂.lift' h₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h₁ h₂ : Set α → Set β<VAR>hh : ∀ s ∈ f, h₁ s ⊆ h₂ s<GOAL>f.lift' h₁ ≤ f.lift' h₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h₁ h₂ : Set α → Set β<VAR>hh : ∀ s ∈ f, h₁ s = h₂ s<GOAL>f.lift' h₁ = f.lift' h₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>m : β → γ<VAR>hh : Monotone h<GOAL>Filter.map m (f.lift' h) = f.lift' (Set.image m ∘ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set β → Set γ<VAR>m : α → β<GOAL>(Filter.map m f).lift' g ≤ f.lift' (g ∘ Set.image m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set β → Set γ<VAR>m : α → β<VAR>hg : Monotone g<GOAL>(Filter.map m f).lift' g = f.lift' (g ∘ Set.image m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>m : γ → β<GOAL>Filter.comap m (f.lift' h) = f.lift' (Set.preimage m ∘ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>m : β → α<VAR>g : Set β → Set γ<VAR>hg : Monotone g<GOAL>(Filter.comap m f).lift' g = f.lift' (g ∘ Set.preimage m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>h : Set α → Set β<VAR>s : Set α<VAR>hh : Monotone h<GOAL>(𝓟 s).lift' h = 𝓟 (h s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>h : Set α → Set β<VAR>a : α<VAR>hh : Monotone h<GOAL>(pure a).lift' h = 𝓟 (h {a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>h : Set α → Set β<VAR>hh : Monotone h<GOAL>⊥.lift' h = 𝓟 (h ∅)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>g : Filter β<GOAL>g ≤ f.lift' h ↔ ∀ s ∈ f, h s ∈ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>t : Set β<GOAL>𝓟 t ≤ f.lift' h ↔ ∀ s ∈ f, t ⊆ h s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder γ<VAR>f : γ → Filter α<VAR>g : γ → Set α → Set β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun c => (f c).lift' (g c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set α → Set β<VAR>h : Set β → Filter γ<VAR>hg : Monotone g<VAR>hh : Monotone h<GOAL>(f.lift' g).lift h = f.lift fun s => h (g s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set α → Set β<VAR>h : Set β → Set γ<VAR>hg : Monotone g<VAR>hh : Monotone h<GOAL>(f.lift' g).lift' h = f.lift' fun s => h (g s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Filter α<VAR>g : Set α → Filter β<VAR>h : Set β → Set γ<VAR>hg : Monotone g<GOAL>(f.lift g).lift' h = f.lift fun s => (g s).lift' h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Set α → Set β<GOAL>(f.lift fun s => f.lift' (g s)) ≤ f.lift' fun s => g s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Set α → Set α → Set β<VAR>hg₁ : ∀ (s : Set α), Monotone fun t => g s t<VAR>hg₂ : ∀ (t : Set α), Monotone fun s => g s t<GOAL>(f.lift fun s => f.lift' (g s)) = f.lift' fun s => g s s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>s : Set β<GOAL>f.lift' h ⊓ 𝓟 s = f.lift' fun t => h t ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>h : Set α → Set β<VAR>hh : Monotone h<GOAL>(f.lift' h).NeBot ↔ ∀ s ∈ f, (h s).Nonempty
<VAR>α : Type u_1<VAR>f : Filter α<GOAL>f.lift' id = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Set β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ∩ g t<GOAL>(iInf f).lift' g = ⨅ i, (f i).lift' g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_4<VAR>f : ι → Filter α<VAR>g : Set α → Set β<VAR>hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t<VAR>hg' : g Set.univ = Set.univ<GOAL>(iInf f).lift' g = ⨅ i, (f i).lift' g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : Filter α<VAR>s : Set α → Set β<VAR>hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂<GOAL>(f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : Filter α<VAR>s : Set α → Set β<GOAL>(f ⊓ g).lift' s ≤ f.lift' s ⊓ g.lift' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter β<VAR>m : α → β<GOAL>Filter.comap m f = f.lift' (Set.preimage m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>f ×ˢ g = f.lift fun s => g.lift' fun t => s ×ˢ t
<VAR>α : Type u_1<VAR>f : Filter α<GOAL>f ×ˢ f = f.lift' fun t => t ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α × α → β<VAR>x : Filter α<VAR>y : Filter β<GOAL>Filter.Tendsto f (x ×ˢ x) y ↔ ∀ W ∈ y, ∃ U ∈ x, ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W
<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Filter β₁<VAR>g₂ : Set α₂ → Filter β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<GOAL>f₁.lift g₁ ×ˢ f₂.lift g₂ = f₁.lift fun s => f₂.lift fun t => g₁ s ×ˢ g₂ t
<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Set β₁<VAR>g₂ : Set α₂ → Set β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<GOAL>f₁.lift' g₁ ×ˢ f₂.lift' g₂ = f₁.lift fun s => f₂.lift' fun t => g₁ s ×ˢ g₂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>f : α → Part β<VAR>g : α → β → Part γ<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => (f x).bind (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>f : α → Part β<VAR>g : α → β → Part γ<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone fun x => (f x).bind (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>f : β → γ<VAR>g : α → Part β<VAR>hg : Monotone g<GOAL>Monotone fun x => Part.map f (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>f : β → γ<VAR>g : α → Part β<VAR>hg : Antitone g<GOAL>Antitone fun x => Part.map f (g x)
<VAR>α : Type u_1<VAR>Preorder α<VAR>β γ : Type u_4<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => Seq.seq (f x) fun x_1 => g x
<VAR>α : Type u_1<VAR>Preorder α<VAR>β γ : Type u_4<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone fun x => Seq.seq (f x) fun x_1 => g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>f : α →o Part β<VAR>g : α →o β → Part γ<VAR>x : α<GOAL>(f.partBind g) x = (f x).bind (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>oi : α ≃o β<GOAL>GaloisConnection ⇑oi ⇑oi.symm
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>hu : Monotone u<VAR>hl : Monotone l<VAR>hul : ∀ (a : α), a ≤ u (l a)<VAR>hlu : ∀ (a : β), l (u a) ≤ a<GOAL>GaloisConnection l u
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<VAR>b : β<GOAL>l a ≤ b ↔ a ≤ u b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<VAR>b : β<GOAL>a ≤ u b → l a ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<VAR>b : β<GOAL>l a ≤ b → a ≤ u b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<GOAL>a ≤ u (l a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : β<GOAL>l (u a) ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>Monotone u
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>Monotone l
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<GOAL>upperBounds (l '' s) = u ⁻¹' upperBounds s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set β<GOAL>lowerBounds (u '' s) = l ⁻¹' lowerBounds s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<GOAL>BddAbove (l '' s) ↔ BddAbove s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set β<GOAL>BddBelow (u '' s) ↔ BddBelow s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<VAR>a : α<VAR>h : IsLUB s a<GOAL>IsLUB (l '' s) (l a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set β<VAR>b : β<VAR>h : IsGLB s b<GOAL>IsGLB (u '' s) (u b)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<GOAL>IsLeast {b | a ≤ u b} (l a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>b : β<GOAL>IsGreatest {a | l a ≤ b} (u b)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<GOAL>IsGLB {b | a ≤ u b} (l a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>b : β<GOAL>IsLUB {a | l a ≤ b} (u b)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>x y z : α<VAR>hxy : x ≤ u (l y)<VAR>hyz : y ≤ u (l z)<GOAL>x ≤ u (l z)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>x y z : β<VAR>hxy : l (u x) ≤ y<VAR>hyz : l (u y) ≤ z<GOAL>l (u x) ≤ z
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>b : β<GOAL>u (l (u b)) = u b
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>u ∘ l ∘ u = u
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>l' : α → β<VAR>u' : β → α<VAR>gc' : GaloisConnection l' u'<VAR>hl : ∀ (a : α), l a = l' a<VAR>b : β<GOAL>u b = u' b
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<GOAL>(∃ b, a = u b) ↔ a = u (l a)
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>z : α<VAR>y : β<GOAL>u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<GOAL>l (u (l a)) = l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>l ∘ u ∘ l = l
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>l' : α → β<VAR>u' : β → α<VAR>gc' : GaloisConnection l' u'<VAR>hu : ∀ (b : β), u b = u' b<VAR>a : α<GOAL>l a = l' a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>b : β<GOAL>(∃ a, b = l a) ↔ b = l (u b)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>x : α<VAR>z : β<GOAL>l x = z ↔ ∀ (y : β), z ≤ y ↔ x ≤ u y
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>OrderTop α<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>x : β<GOAL>u x = ⊤ ↔ l ⊤ ≤ x
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderTop β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>u ⊤ = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>x : α<GOAL>l x = ⊥ ↔ x ≤ u ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>OrderBot β<VAR>OrderBot α<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>l ⊥ = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>a₁ a₂ : α<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂
<VAR>α : Type u<VAR>β : Type v<VAR>b₁ b₂ : β<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>f : ι → α<GOAL>l (iSup f) = ⨆ i, l (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>f : (i : ι) → κ i → α<GOAL>l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>f : ι → β<GOAL>u (iInf f) = ⨅ i, u (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>f : (i : ι) → κ i → β<GOAL>u (⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, u (f i j)
<VAR>α : Type u<VAR>β : Type v<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<GOAL>l (sSup s) = ⨆ a ∈ s, l a
<VAR>α : Type u<VAR>β : Type v<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set β<GOAL>u (sInf s) = ⨅ a ∈ s, u a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : α<VAR>b : β<GOAL>b < l a ↔ u b < a
<VAR>α : Type u<VAR>pα : Preorder α<GOAL>GaloisConnection id id
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>l1 : α → β<VAR>u1 : β → α<VAR>l2 : β → γ<VAR>u2 : γ → β<VAR>gc1 : GaloisConnection l1 u1<VAR>gc2 : GaloisConnection l2 u2<GOAL>GaloisConnection (l2 ∘ l1) (u1 ∘ u2)
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>β : ι → Type w<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → Preorder (β i)<VAR>l : (i : ι) → α i → β i<VAR>u : (i : ι) → β i → α i<VAR>gc : ∀ (i : ι), GaloisConnection (l i) (u i)<GOAL>GaloisConnection (fun a i => l i (a i)) fun b i => u i (b i)
<VAR>α : Type u<VAR>β : Type v<VAR>BooleanAlgebra α<VAR>BooleanAlgebra β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl)
<VAR>X : Type u_2<VAR>Preorder X<VAR>Y : Type u_3<VAR>Preorder Y<VAR>Z : Type u_4<VAR>Preorder Z<VAR>W : Type u_5<VAR>PartialOrder W<VAR>lYX : X → Y<VAR>uXY : Y → X<VAR>hXY : GaloisConnection lYX uXY<VAR>lWZ : Z → W<VAR>uZW : W → Z<VAR>hZW : GaloisConnection lWZ uZW<VAR>lWY : Y → W<VAR>uYW : W → Y<VAR>hWY : GaloisConnection lWY uYW<VAR>lZX : X → Z<VAR>uXZ : Z → X<VAR>hXZ : GaloisConnection lZX uXZ<VAR>h : ∀ (w : W), uXZ (uZW w) = uXY (uYW w)<VAR>x : X<GOAL>lWZ (lZX x) = lWY (lYX x)
<VAR>X : Type u_2<VAR>PartialOrder X<VAR>Y : Type u_3<VAR>Preorder Y<VAR>Z : Type u_4<VAR>Preorder Z<VAR>W : Type u_5<VAR>Preorder W<VAR>lYX : X → Y<VAR>uXY : Y → X<VAR>hXY : GaloisConnection lYX uXY<VAR>lWZ : Z → W<VAR>uZW : W → Z<VAR>hZW : GaloisConnection lWZ uZW<VAR>lWY : Y → W<VAR>uYW : W → Y<VAR>hWY : GaloisConnection lWY uYW<VAR>lZX : X → Z<VAR>uXZ : Z → X<VAR>hXZ : GaloisConnection lZX uXZ<VAR>h : ∀ (x : X), lWZ (lZX x) = lWY (lYX x)<VAR>w : W<GOAL>uXZ (uZW w) = uXY (uYW w)
<VAR>X : Type u_2<VAR>PartialOrder X<VAR>Y : Type u_3<VAR>Preorder Y<VAR>Z : Type u_4<VAR>Preorder Z<VAR>W : Type u_5<VAR>PartialOrder W<VAR>lYX : X → Y<VAR>uXY : Y → X<VAR>hXY : GaloisConnection lYX uXY<VAR>lWZ : Z → W<VAR>uZW : W → Z<VAR>hZW : GaloisConnection lWZ uZW<VAR>lWY : Y → W<VAR>uYW : W → Y<VAR>hWY : GaloisConnection lWY uYW<VAR>lZX : X → Z<VAR>uXZ : Z → X<VAR>hXZ : GaloisConnection lZX uXZ<GOAL>(∀ (w : W), uXZ (uZW w) = uXY (uYW w)) ↔ ∀ (x : X), lWZ (lZX x) = lWY (lYX x)
<VAR>α : Type u<VAR>CompleteSemilatticeSup α<GOAL>GaloisConnection sSup Set.Iic
<VAR>α : Type u<VAR>CompleteSemilatticeInf α<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>l : α → β → γ<VAR>u₁ : β → γ → α<VAR>u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)<GOAL>sSup (Set.image2 l s t) = l (sSup s) (sSup t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>l : α → β → γ<VAR>u₁ : β → γ → α<VAR>u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)<GOAL>sSup (Set.image2 l s t) = l (sSup s) (sInf t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>l : α → β → γ<VAR>u₁ : β → γ → α<VAR>u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)<GOAL>sSup (Set.image2 l s t) = l (sInf s) (sSup t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>l : α → β → γ<VAR>u₁ : β → γ → α<VAR>u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)<GOAL>sSup (Set.image2 l s t) = l (sInf s) (sInf t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>u : α → β → γ<VAR>l₁ : β → γ → α<VAR>l₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)<GOAL>sInf (Set.image2 u s t) = u (sInf s) (sInf t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>u : α → β → γ<VAR>l₁ : β → γ → α<VAR>l₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)<VAR>h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)<GOAL>sInf (Set.image2 u s t) = u (sInf s) (sSup t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>u : α → β → γ<VAR>l₁ : β → γ → α<VAR>l₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)<VAR>h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)<GOAL>sInf (Set.image2 u s t) = u (sSup s) (sInf t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>s : Set α<VAR>t : Set β<VAR>u : α → β → γ<VAR>l₁ : β → γ → α<VAR>l₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)<VAR>h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)<GOAL>sInf (Set.image2 u s t) = u (sSup s) (sSup t)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>s : Set α<GOAL>BddAbove (⇑e '' s) ↔ BddAbove s