ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>g.NeBot<VAR>Nonempty α<GOAL>(f.coprod g).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<GOAL>(𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
<VAR>α₁ : Type u<VAR>α₂ : Type v<VAR>β₁ : Type w<VAR>β₂ : Type x<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>m₁ : α₁ → β₁<VAR>m₂ : α₂ → β₂<GOAL>Filter.map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (Filter.map m₁ f₁).coprod (Filter.map m₂ f₂)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ι : Type u_8<VAR>a : α<VAR>b : β<VAR>i : ι<GOAL>(Filter.map (fun x => b) (𝓟 {a})).coprod (Filter.map id (𝓟 {i})) = 𝓟 ({b} ×ˢ Set.univ ∪ Set.univ ×ˢ {i})
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ι : Type u_8<VAR>a : α<VAR>b : β<VAR>i : ι<GOAL>Filter.map (Prod.map (fun x => b) id) ((𝓟 {a}).coprod (𝓟 {i})) = 𝓟 ({b} ×ˢ Set.univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_6<VAR>f : α → γ<VAR>g : β → δ<VAR>a : Filter α<VAR>b : Filter β<VAR>c : Filter γ<VAR>d : Filter δ<VAR>hf : Filter.Tendsto f a c<VAR>hg : Filter.Tendsto g b d<GOAL>Filter.Tendsto (Prod.map f g) (a.coprod b) (c.coprod d)
<VAR>α : Type u_1<VAR>Ixx : α → α → Set α<VAR>l₁ : Filter α<VAR>l₂ : outParam (Filter α)<VAR>self : Filter.TendstoIxxClass Ixx l₁ l₂<GOAL>Filter.Tendsto (fun p => Ixx p.1 p.2) (l₁ ×ˢ l₁) (Filter.smallSets l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>l₁ l₂ : Filter α<VAR>Filter.TendstoIxxClass Set.Icc l₁ l₂<VAR>lb : Filter β<VAR>u₁ u₂ : β → α<VAR>h₁ : Filter.Tendsto u₁ lb l₁<VAR>h₂ : Filter.Tendsto u₂ lb l₁<GOAL>Filter.Tendsto (fun x => Set.Icc (u₁ x) (u₂ x)) lb l₂.smallSets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>l₁ l₂ : Filter α<VAR>Filter.TendstoIxxClass Set.Ioc l₁ l₂<VAR>lb : Filter β<VAR>u₁ u₂ : β → α<VAR>h₁ : Filter.Tendsto u₁ lb l₁<VAR>h₂ : Filter.Tendsto u₂ lb l₁<GOAL>Filter.Tendsto (fun x => Set.Ioc (u₁ x) (u₂ x)) lb l₂.smallSets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>l₁ l₂ : Filter α<VAR>Filter.TendstoIxxClass Set.Ico l₁ l₂<VAR>lb : Filter β<VAR>u₁ u₂ : β → α<VAR>h₁ : Filter.Tendsto u₁ lb l₁<VAR>h₂ : Filter.Tendsto u₂ lb l₁<GOAL>Filter.Tendsto (fun x => Set.Ico (u₁ x) (u₂ x)) lb l₂.smallSets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>l₁ l₂ : Filter α<VAR>Filter.TendstoIxxClass Set.Ioo l₁ l₂<VAR>lb : Filter β<VAR>u₁ u₂ : β → α<VAR>h₁ : Filter.Tendsto u₁ lb l₁<VAR>h₂ : Filter.Tendsto u₂ lb l₁<GOAL>Filter.Tendsto (fun x => Set.Ioo (u₁ x) (u₂ x)) lb l₂.smallSets
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Ixx : α → α → Set α<GOAL>Filter.TendstoIxxClass Ixx (𝓟 s) (𝓟 t) ↔ ∀ x ∈ s, ∀ y ∈ s, Ixx x y ⊆ t
<VAR>α : Type u_1<VAR>l₁ l₁' l₂ l₂' : Filter α<VAR>Ixx : α → α → Set α<VAR>h : Filter.TendstoIxxClass Ixx l₁ l₂<VAR>h' : Filter.TendstoIxxClass Ixx l₁' l₂'<GOAL>Filter.TendstoIxxClass Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂')
<VAR>α : Type u_1<VAR>l₁ l₂ : Filter α<VAR>Ixx Ixx' : α → α → Set α<VAR>h : ∀ (a b : α), Ixx a b ⊆ Ixx' a b<VAR>h' : Filter.TendstoIxxClass Ixx' l₁ l₂<GOAL>Filter.TendstoIxxClass Ixx l₁ l₂
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>l : Filter α<VAR>hl : l.HasBasis p s<VAR>Ixx : α → α → Set α<VAR>H : ∀ (i : ι), p i → ∀ x ∈ s i, ∀ y ∈ s i, Ixx x y ⊆ s i<GOAL>Filter.TendstoIxxClass Ixx l l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>l : Filter α<VAR>Filter.TendstoIxxClass Set.Icc l l<VAR>f g : β → α<VAR>lb : Filter β<VAR>hf : Filter.Tendsto f lb l<VAR>hg : Filter.Tendsto g lb l<GOAL>Filter.Tendsto (fun x => Set.uIcc (f x) (g x)) lb l.smallSets
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>p : Prop<GOAL>IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → p
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<GOAL>IsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<GOAL>IsMaxOn f s a ↔ ∀ x ∈ s, f x ≤ f a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>a : α<GOAL>IsMinOn f Set.univ a ↔ ∀ (x : α), f a ≤ f x
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>a : α<GOAL>IsMaxOn f Set.univ a ↔ ∀ (x : α), f x ≤ f a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>h : IsMinFilter f l a<GOAL>Filter.Tendsto f l (𝓟 (Set.Ici (f a)))
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>h : IsMaxFilter f l a<GOAL>Filter.Tendsto f l (𝓟 (Set.Iic (f a)))
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<GOAL>IsMinFilter f l a → IsExtrFilter f l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<GOAL>IsMaxFilter f l a → IsExtrFilter f l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h : IsMinOn f s a<GOAL>IsExtrOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h : IsMaxOn f s a<GOAL>IsExtrOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>a : α<VAR>b : β<GOAL>IsMinFilter (fun x => b) l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>a : α<VAR>b : β<GOAL>IsMaxFilter (fun x => b) l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>a : α<VAR>b : β<GOAL>IsExtrFilter (fun x => b) l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>s : Set α<VAR>a : α<VAR>b : β<GOAL>IsMinOn (fun x => b) s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>s : Set α<VAR>a : α<VAR>b : β<GOAL>IsMaxOn (fun x => b) s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>s : Set α<VAR>a : α<VAR>b : β<GOAL>IsExtrOn (fun x => b) s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<GOAL>IsMinFilter (⇑OrderDual.toDual ∘ f) l a ↔ IsMaxFilter f l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<GOAL>IsMaxFilter (⇑OrderDual.toDual ∘ f) l a ↔ IsMinFilter f l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<GOAL>IsExtrFilter (⇑OrderDual.toDual ∘ f) l a ↔ IsExtrFilter f l a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<GOAL>IsMinOn (⇑OrderDual.toDual ∘ f) s a ↔ IsMaxOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<GOAL>IsMaxOn (⇑OrderDual.toDual ∘ f) s a ↔ IsMinOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<GOAL>IsExtrOn (⇑OrderDual.toDual ∘ f) s a ↔ IsExtrOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>l' : Filter α<VAR>h : IsMinFilter f l a<VAR>hl : l' ≤ l<GOAL>IsMinFilter f l' a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>l' : Filter α<VAR>h : IsMaxFilter f l a<VAR>hl : l' ≤ l<GOAL>IsMaxFilter f l' a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>l' : Filter α<VAR>h : IsExtrFilter f l a<VAR>hl : l' ≤ l<GOAL>IsExtrFilter f l' a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>h : IsMinFilter f l a<VAR>l' : Filter α<GOAL>IsMinFilter f (l ⊓ l') a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>h : IsMaxFilter f l a<VAR>l' : Filter α<GOAL>IsMaxFilter f (l ⊓ l') a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>h : IsExtrFilter f l a<VAR>l' : Filter α<GOAL>IsExtrFilter f (l ⊓ l') a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set α<VAR>hf : IsMinOn f t a<VAR>h : s ⊆ t<GOAL>IsMinOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set α<VAR>hf : IsMaxOn f t a<VAR>h : s ⊆ t<GOAL>IsMaxOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set α<VAR>hf : IsExtrOn f t a<VAR>h : s ⊆ t<GOAL>IsExtrOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMinOn f s a<VAR>t : Set α<GOAL>IsMinOn f (s ∩ t) a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMaxOn f s a<VAR>t : Set α<GOAL>IsMaxOn f (s ∩ t) a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsExtrOn f s a<VAR>t : Set α<GOAL>IsExtrOn f (s ∩ t) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>hf : IsMinFilter f l a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsMinFilter (g ∘ f) l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>hf : IsMaxFilter f l a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsMaxFilter (g ∘ f) l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>hf : IsExtrFilter f l a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsExtrFilter (g ∘ f) l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>hf : IsMinFilter f l a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsMaxFilter (g ∘ f) l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>hf : IsMaxFilter f l a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsMinFilter (g ∘ f) l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>hf : IsExtrFilter f l a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsExtrFilter (g ∘ f) l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMinOn f s a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsMinOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMaxOn f s a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsMaxOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsExtrOn f s a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsExtrOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMinOn f s a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsMaxOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMaxOn f s a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsMinOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsExtrOn f s a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsExtrOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>Preorder δ<VAR>op : β → γ → δ<VAR>hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op<VAR>hf : IsMinFilter f l a<VAR>g : α → γ<VAR>hg : IsMinFilter g l a<GOAL>IsMinFilter (fun x => op (f x) (g x)) l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>l : Filter α<VAR>a : α<VAR>Preorder δ<VAR>op : β → γ → δ<VAR>hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op<VAR>hf : IsMaxFilter f l a<VAR>g : α → γ<VAR>hg : IsMaxFilter g l a<GOAL>IsMaxFilter (fun x => op (f x) (g x)) l a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>Preorder δ<VAR>op : β → γ → δ<VAR>hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op<VAR>hf : IsMinOn f s a<VAR>g : α → γ<VAR>hg : IsMinOn g s a<GOAL>IsMinOn (fun x => op (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>Preorder δ<VAR>op : β → γ → δ<VAR>hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op<VAR>hf : IsMaxOn f s a<VAR>g : α → γ<VAR>hg : IsMaxOn g s a<GOAL>IsMaxOn (fun x => op (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>g : δ → α<VAR>l' : Filter δ<VAR>b : δ<VAR>hf : IsMinFilter f l (g b)<VAR>hg : Filter.Tendsto g l' l<GOAL>IsMinFilter (f ∘ g) l' b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>g : δ → α<VAR>l' : Filter δ<VAR>b : δ<VAR>hf : IsMaxFilter f l (g b)<VAR>hg : Filter.Tendsto g l' l<GOAL>IsMaxFilter (f ∘ g) l' b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>g : δ → α<VAR>l' : Filter δ<VAR>b : δ<VAR>hf : IsExtrFilter f l (g b)<VAR>hg : Filter.Tendsto g l' l<GOAL>IsExtrFilter (f ∘ g) l' b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsMinOn f s (g b)<GOAL>IsMinOn (f ∘ g) (g ⁻¹' s) b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsMaxOn f s (g b)<GOAL>IsMaxOn (f ∘ g) (g ⁻¹' s) b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsExtrOn f s (g b)<GOAL>IsExtrOn (f ∘ g) (g ⁻¹' s) b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsMinOn f s a<VAR>hg : Set.MapsTo g t s<VAR>ha : g b = a<GOAL>IsMinOn (f ∘ g) t b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsMaxOn f s a<VAR>hg : Set.MapsTo g t s<VAR>ha : g b = a<GOAL>IsMaxOn (f ∘ g) t b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsExtrOn f s a<VAR>hg : Set.MapsTo g t s<VAR>ha : g b = a<GOAL>IsExtrOn (f ∘ g) t b
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommMonoid β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMinFilter f l a<VAR>hg : IsMinFilter g l a<GOAL>IsMinFilter (fun x => f x + g x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommMonoid β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMaxFilter f l a<VAR>hg : IsMaxFilter g l a<GOAL>IsMaxFilter (fun x => f x + g x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommMonoid β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMinOn f s a<VAR>hg : IsMinOn g s a<GOAL>IsMinOn (fun x => f x + g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommMonoid β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMaxOn f s a<VAR>hg : IsMaxOn g s a<GOAL>IsMaxOn (fun x => f x + g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMinFilter f l a<GOAL>IsMaxFilter (fun x => -f x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMaxFilter f l a<GOAL>IsMinFilter (fun x => -f x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsExtrFilter f l a<GOAL>IsExtrFilter (fun x => -f x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMinOn f s a<GOAL>IsMaxOn (fun x => -f x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMaxOn f s a<GOAL>IsMinOn (fun x => -f x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsExtrOn f s a<GOAL>IsExtrOn (fun x => -f x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMinFilter f l a<VAR>hg : IsMaxFilter g l a<GOAL>IsMinFilter (fun x => f x - g x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMaxFilter f l a<VAR>hg : IsMinFilter g l a<GOAL>IsMaxFilter (fun x => f x - g x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMinOn f s a<VAR>hg : IsMaxOn g s a<GOAL>IsMinOn (fun x => f x - g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMaxOn f s a<VAR>hg : IsMinOn g s a<GOAL>IsMaxOn (fun x => f x - g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMinFilter f l a<VAR>hg : IsMinFilter g l a<GOAL>IsMinFilter (fun x => f x ⊔ g x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMaxFilter f l a<VAR>hg : IsMaxFilter g l a<GOAL>IsMaxFilter (fun x => f x ⊔ g x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMinOn f s a<VAR>hg : IsMinOn g s a<GOAL>IsMinOn (fun x => f x ⊔ g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMaxOn f s a<VAR>hg : IsMaxOn g s a<GOAL>IsMaxOn (fun x => f x ⊔ g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMinFilter f l a<VAR>hg : IsMinFilter g l a<GOAL>IsMinFilter (fun x => f x ⊓ g x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMaxFilter f l a<VAR>hg : IsMaxFilter g l a<GOAL>IsMaxFilter (fun x => f x ⊓ g x) l a
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMinOn f s a<VAR>hg : IsMinOn g s a<GOAL>IsMinOn (fun x => f x ⊓ g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMaxOn f s a<VAR>hg : IsMaxOn g s a<GOAL>IsMaxOn (fun x => f x ⊓ g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMinFilter f l a<VAR>hg : IsMinFilter g l a<GOAL>IsMinFilter (fun x => min (f x) (g x)) l a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMaxFilter f l a<VAR>hg : IsMaxFilter g l a<GOAL>IsMaxFilter (fun x => min (f x) (g x)) l a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMinOn f s a<VAR>hg : IsMinOn g s a<GOAL>IsMinOn (fun x => min (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMaxOn f s a<VAR>hg : IsMaxOn g s a<GOAL>IsMaxOn (fun x => min (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMinFilter f l a<VAR>hg : IsMinFilter g l a<GOAL>IsMinFilter (fun x => max (f x) (g x)) l a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hf : IsMaxFilter f l a<VAR>hg : IsMaxFilter g l a<GOAL>IsMaxFilter (fun x => max (f x) (g x)) l a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMinOn f s a<VAR>hg : IsMinOn g s a<GOAL>IsMinOn (fun x => max (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsMaxOn f s a<VAR>hg : IsMaxOn g s a<GOAL>IsMaxOn (fun x => max (f x) (g x)) s a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hle : g ≤ᶠ[l] f<VAR>hfga : f a = g a<VAR>h : IsMaxFilter f l a<GOAL>IsMaxFilter g l a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>h : IsMaxFilter f l a<VAR>heq : f =ᶠ[l] g<VAR>hfga : f a = g a<GOAL>IsMaxFilter g l a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>heq : f =ᶠ[l] g<VAR>hfga : f a = g a<GOAL>IsMaxFilter f l a ↔ IsMaxFilter g l a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hle : f ≤ᶠ[l] g<VAR>hfga : f a = g a<VAR>h : IsMinFilter f l a<GOAL>IsMinFilter g l a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>h : IsMinFilter f l a<VAR>heq : f =ᶠ[l] g<VAR>hfga : f a = g a<GOAL>IsMinFilter g l a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>heq : f =ᶠ[l] g<VAR>hfga : f a = g a<GOAL>IsMinFilter f l a ↔ IsMinFilter g l a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>h : IsExtrFilter f l a<VAR>heq : f =ᶠ[l] g<VAR>hfga : f a = g a<GOAL>IsExtrFilter g l a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>heq : f =ᶠ[l] g<VAR>hfga : f a = g a<GOAL>IsExtrFilter f l a ↔ IsExtrFilter g l a
<VAR>α : Type u<VAR>β : Type v<VAR>ConditionallyCompleteLinearOrder α<VAR>f : β → α<VAR>s : Set β<VAR>x₀ : β<VAR>hx₀ : x₀ ∈ s<VAR>h : IsMaxOn f s x₀<GOAL>⨆ x, f ↑x = f x₀
<VAR>α : Type u<VAR>β : Type v<VAR>ConditionallyCompleteLinearOrder α<VAR>f : β → α<VAR>s : Set β<VAR>x₀ : β<VAR>hx₀ : x₀ ∈ s<VAR>h : IsMinOn f s x₀<GOAL>⨅ x, f ↑x = f x₀
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>s : Set α<VAR>t : Set β<GOAL>t ⊆ intentClosure r s ↔ s ⊆ extentClosure r t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ intentClosure r) (extentClosure r ∘ ⇑OrderDual.ofDual)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>t : Set β<GOAL>intentClosure (Function.swap r) t = extentClosure r t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>s : Set α<GOAL>extentClosure (Function.swap r) s = intentClosure r s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>intentClosure r ∅ = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>extentClosure r ∅ = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>s₁ s₂ : Set α<GOAL>intentClosure r (s₁ ∪ s₂) = intentClosure r s₁ ∩ intentClosure r s₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>t₁ t₂ : Set β<GOAL>extentClosure r (t₁ ∪ t₂) = extentClosure r t₁ ∩ extentClosure r t₂
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>f : ι → Set α<GOAL>intentClosure r (⋃ i, f i) = ⋂ i, intentClosure r (f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>f : ι → Set β<GOAL>extentClosure r (⋃ i, f i) = ⋂ i, extentClosure r (f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>κ : ι → Sort u_5<VAR>r : α → β → Prop<VAR>f : (i : ι) → κ i → Set α<GOAL>intentClosure r (⋃ i, ⋃ j, f i j) = ⋂ i, ⋂ j, intentClosure r (f i j)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>κ : ι → Sort u_5<VAR>r : α → β → Prop<VAR>f : (i : ι) → κ i → Set β<GOAL>extentClosure r (⋃ i, ⋃ j, f i j) = ⋂ i, ⋂ j, extentClosure r (f i j)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>s : Set α<GOAL>s ⊆ extentClosure r (intentClosure r s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>t : Set β<GOAL>t ⊆ intentClosure r (extentClosure r t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>s : Set α<GOAL>intentClosure r (extentClosure r (intentClosure r s)) = intentClosure r s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>t : Set β<GOAL>extentClosure r (intentClosure r (extentClosure r t)) = extentClosure r t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>Antitone (intentClosure r)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>Antitone (extentClosure r)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>self : Concept α β r<GOAL>intentClosure r self.toProd.1 = self.toProd.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>self : Concept α β r<GOAL>extentClosure r self.toProd.2 = self.toProd.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<VAR>h : c.toProd.1 = d.toProd.1<GOAL>c = d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<VAR>h : c.toProd.2 = d.toProd.2<GOAL>c = d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>Function.Injective fun c => c.toProd.1