ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Filter.limsup u f \ a = Filter.limsup (fun b => u b \ a) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>f.NeBot<VAR>a : α<GOAL>Filter.liminf u f \ a = Filter.liminf (fun b => u b \ a) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>f.NeBot<VAR>a : α<GOAL>a \ Filter.limsup u f = Filter.liminf (fun b => a \ u b) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>a \ Filter.liminf u f = Filter.limsup (fun b => a \ u b) f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>a ∈ Filter.liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>a ∈ Filter.limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<GOAL>Filter.blimsup s Filter.cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite}
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<GOAL>Filter.bliminf s Filter.cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : ι → Set α<GOAL>Filter.limsup s Filter.cofinite = {x | {n | x ∈ s n}.Infinite}
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : ι → Set α<GOAL>Filter.liminf s Filter.cofinite = {x | {n | x ∉ s n}.Finite}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>l : Filter β<VAR>b : ι → Set β<VAR>q : ι → Prop<VAR>hl : l.HasBasis q b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>hx : x ∈ Filter.blimsup u l p<GOAL>∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>l : Filter β<VAR>b : ι → Set β<VAR>hl : l.HasBasis (fun x => True) b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>hx : x ∈ Filter.blimsup u l p<GOAL>∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
<VAR>α : Type u_1<VAR>f : Filter α<VAR>ConditionallyCompleteLinearOrder α<VAR>a : α<VAR>hf : Filter.IsCobounded (fun x x_1 => x ≤ x_1) f := by isBoundedDefault<VAR>h : a < f.limsSup<GOAL>∃ᶠ (n : α) in f, a < n
<VAR>α : Type u_1<VAR>f : Filter α<VAR>ConditionallyCompleteLinearOrder α<VAR>a : α<VAR>hf : Filter.IsCobounded (fun x x_1 => x ≥ x_1) f := by isBoundedDefault<VAR>h : f.limsInf < a<GOAL>∃ᶠ (n : α) in f, n < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>ConditionallyCompleteLinearOrder β<VAR>u : α → β<VAR>b : β<VAR>h : b < Filter.liminf u f<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<GOAL>∀ᶠ (a : α) in f, b < u a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>ConditionallyCompleteLinearOrder β<VAR>u : α → β<VAR>b : β<VAR>h : Filter.limsup u f < b<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<GOAL>∀ᶠ (a : α) in f, u a < b
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu_le : ∃ᶠ (x : α) in f, b ≤ u x<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<GOAL>b ≤ Filter.limsup u f
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu_le : ∃ᶠ (x : α) in f, u x ≤ b<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<GOAL>Filter.liminf u f ≤ b
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>h : b < Filter.limsup u f<GOAL>∃ᶠ (x : α) in f, b < u x
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>h : Filter.liminf u f < b<GOAL>∃ᶠ (x : α) in f, u x < b
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h₁ : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>h₂ : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<GOAL>Filter.limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h₁ : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>h₂ : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<GOAL>x ≤ Filter.limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h₁ : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>h₂ : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<GOAL>x ≤ Filter.liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y < u a
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h₁ : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>h₂ : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<GOAL>Filter.liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a < y
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>f : Filter α<VAR>b : α<VAR>h : Filter.IsBounded (fun x x_1 => x ≤ x_1) f<VAR>l : f.limsSup < b<GOAL>∀ᶠ (a : α) in f, a < b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>f : Filter α<VAR>b : α<GOAL>Filter.IsBounded (fun x x_1 => x ≥ x_1) f → b < f.limsInf → ∀ᶠ (a : α) in f, b < a
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ConditionallyCompleteLinearOrder α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>Countable (Subtype p)<VAR>Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>hs : ∀ (j : Subtype p), (s ↑j).Nonempty<VAR>H : ∃ j, BddBelow (Set.range fun i => f ↑i)<GOAL>Filter.liminf f v = ⨆ j, ⨅ i, f ↑i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ConditionallyCompleteLinearOrder α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>Countable (Subtype p)<VAR>Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<GOAL>Filter.liminf f v = if ∃ j, s ↑j = ∅ then sSup Set.univ else if ∀ (j : Subtype p), ¬BddBelow (Set.range fun i => f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ConditionallyCompleteLinearOrder α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>Countable (Subtype p)<VAR>Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>hs : ∀ (j : Subtype p), (s ↑j).Nonempty<VAR>H : ∃ j, BddAbove (Set.range fun i => f ↑i)<GOAL>Filter.limsup f v = ⨅ j, ⨆ i, f ↑i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ConditionallyCompleteLinearOrder α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>Countable (Subtype p)<VAR>Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<GOAL>Filter.limsup f v = if ∃ j, s ↑j = ∅ then sInf Set.univ else if ∀ (j : Subtype p), ¬BddAbove (Set.range fun i => f ↑i) then sInf ∅ else ⨅ j, ⨆ i, f ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Nonempty β<VAR>LinearOrder β<VAR>Preorder γ<VAR>NoMaxOrder γ<VAR>g : β → γ<VAR>f : α → β<VAR>l : Filter α<VAR>hg : Monotone g<VAR>hg' : Filter.Tendsto g Filter.atTop Filter.atTop<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Nonempty β<VAR>LinearOrder β<VAR>Preorder γ<VAR>NoMinOrder γ<VAR>g : β → γ<VAR>f : α → β<VAR>l : Filter α<VAR>hg : Monotone g<VAR>hg' : Filter.Tendsto g Filter.atBot Filter.atBot<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Nonempty β<VAR>LinearOrder β<VAR>Preorder γ<VAR>NoMaxOrder γ<VAR>g : β → γ<VAR>f : α → β<VAR>l : Filter α<VAR>hg : Antitone g<VAR>hg' : Filter.Tendsto g Filter.atBot Filter.atTop<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Nonempty β<VAR>LinearOrder β<VAR>Preorder γ<VAR>NoMinOrder γ<VAR>g : β → γ<VAR>f : α → β<VAR>l : Filter α<VAR>hg : Antitone g<VAR>hg' : Filter.Tendsto g Filter.atTop Filter.atBot<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>v : α → β<VAR>l : β → γ<VAR>u : γ → β<VAR>gc : GaloisConnection l u<VAR>hlv : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x) := by isBoundedDefault<VAR>hv_co : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v := by isBoundedDefault<GOAL>l (Filter.limsup v f) ≤ Filter.limsup (fun x => l (v x)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_6<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>hu_co : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>hgu : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x) := by isBoundedDefault<VAR>hgu_co : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x) := by isBoundedDefault<GOAL>g (Filter.limsup u f) = Filter.limsup (fun x => g (u x)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_6<VAR>ConditionallyCompleteLattice β<VAR>ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>hu_co : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>hgu : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f fun x => g (u x) := by isBoundedDefault<VAR>hgu_co : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f fun x => g (u x) := by isBoundedDefault<GOAL>g (Filter.liminf u f) = Filter.liminf (fun x => g (u x)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : Filter α<VAR>u v : α → β<VAR>h : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u ∨ Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun a => max (u a) (v a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u v : α → β<VAR>h₁ : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>h₂ : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v := by isBoundedDefault<VAR>h₃ : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>h₄ : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f v := by isBoundedDefault<GOAL>Filter.limsup (fun a => max (u a) (v a)) f = max (Filter.limsup u f) (Filter.limsup v f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u v : α → β<VAR>h₁ : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>h₂ : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f v := by isBoundedDefault<VAR>h₃ : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>h₄ : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f v := by isBoundedDefault<GOAL>Filter.liminf (fun a => min (u a) (v a)) f = min (Filter.liminf u f) (Filter.liminf v f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>LinearOrder β<VAR>Nonempty β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h : ∀ i ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup' hs fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>LinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h : ∃ i ∈ s, Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup' hs fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>LinearOrder β<VAR>OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>LinearOrder β<VAR>Nonempty β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h : ∀ i ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f (F i)<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f fun a => s.inf' hs fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>LinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h : ∃ i ∈ s, Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f (F i)<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f fun a => s.inf' hs fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>LinearOrder β<VAR>OrderTop β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f (F i)<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f fun a => s.inf fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i) := by exact fun _ _ ↦ by isBoundedDefault<VAR>h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i) := by exact fun _ _ ↦ by isBoundedDefault<GOAL>Filter.limsup (fun a => s.sup' hs fun i => F i a) f = s.sup' hs fun i => Filter.limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>ConditionallyCompleteLinearOrder β<VAR>OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i) := by exact fun _ _ ↦ by isBoundedDefault<VAR>h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i) := by exact fun _ _ ↦ by isBoundedDefault<GOAL>Filter.limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => Filter.limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f (F i) := by exact fun _ _ ↦ by isBoundedDefault<VAR>h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f (F i) := by exact fun _ _ ↦ by isBoundedDefault<GOAL>Filter.liminf (fun a => s.inf' hs fun i => F i a) f = s.inf' hs fun i => Filter.liminf (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>ConditionallyCompleteLinearOrder β<VAR>OrderTop β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f (F i) := by exact fun _ _ ↦ by isBoundedDefault<VAR>h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f (F i) := by exact fun _ _ ↦ by isBoundedDefault<GOAL>Filter.liminf (fun a => s.inf fun i => F i a) f = s.inf fun i => Filter.liminf (F i) f
<VAR>R : Type u_6<VAR>F : Filter R<VAR>LinearOrder R<VAR>F.NeBot<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≤ x_1) F<GOAL>∃ l, ∃ᶠ (x : R) in F, l ≤ x
<VAR>R : Type u_6<VAR>F : Filter R<VAR>LinearOrder R<VAR>F.NeBot<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≥ x_1) F<GOAL>∃ u, ∃ᶠ (x : R) in F, x ≤ u
<VAR>R : Type u_6<VAR>F : Filter R<VAR>LinearOrder R<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<GOAL>Filter.IsCobounded (fun x x_1 => x ≤ x_1) F
<VAR>R : Type u_6<VAR>F : Filter R<VAR>LinearOrder R<VAR>u : R<VAR>freq_le : ∃ᶠ (r : R) in F, r ≤ u<GOAL>Filter.IsCobounded (fun x x_1 => x ≥ x_1) F
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>LinearOrder R<VAR>LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<GOAL>∃ᶠ (x' : S) in Filter.map f F, f l ≤ x'
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>LinearOrder R<VAR>LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>u : R<VAR>freq_le : ∃ᶠ (x : R) in F, x ≤ u<GOAL>∃ᶠ (y : S) in Filter.map f F, y ≤ f u
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>LinearOrder R<VAR>LinearOrder S<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>l : R<VAR>frbdd : ∃ᶠ (x : R) in F, l ≤ x<GOAL>∃ᶠ (y : S) in Filter.map f F, y ≤ f l
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>LinearOrder R<VAR>LinearOrder S<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>u : R<VAR>frbdd : ∃ᶠ (x : R) in F, x ≤ u<GOAL>∃ᶠ (y : S) in Filter.map f F, f u ≤ y
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>LinearOrder R<VAR>LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>F.NeBot<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≤ x_1) F<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) F f
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>LinearOrder R<VAR>LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>F.NeBot<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≥ x_1) F<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) F f
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>LinearOrder R<VAR>LinearOrder S<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>F.NeBot<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≥ x_1) F<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) F f
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>LinearOrder R<VAR>LinearOrder S<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>F.NeBot<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≤ x_1) F<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) F f
<VAR>α : Type u<VAR>self : Order.Frame.MinimalAxioms α<VAR>a : α<VAR>s : Set α<GOAL>a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
<VAR>α : Type u<VAR>self : Order.Coframe.MinimalAxioms α<VAR>a : α<VAR>s : Set α<GOAL>⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
<VAR>α : Type u_1<VAR>self : Order.Frame α<VAR>a : α<VAR>s : Set α<GOAL>a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
<VAR>α : Type u_1<VAR>self : Order.Coframe α<VAR>a : α<VAR>s : Set α<GOAL>⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
<VAR>α : Type u<VAR>self : CompletelyDistribLattice.MinimalAxioms α<VAR>ι : Type u<VAR>κ : ι → Type u<VAR>f : (a : ι) → κ a → α<GOAL>⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
<VAR>α : Type u<VAR>self : CompletelyDistribLattice α<VAR>ι : Type u<VAR>κ : ι → Type u<VAR>f : (a : ι) → κ a → α<GOAL>⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>CompleteLattice α<VAR>f : (a : ι) → κ a → α<GOAL>⨆ g, ⨅ a, f a (g a) ≤ ⨅ a, ⨆ b, f a b
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>CompleteLattice α<VAR>f : (a : ι) → κ a → α<GOAL>⨆ a, ⨅ b, f a b ≤ ⨅ g, ⨆ a, f a (g a)
<VAR>α : Type u<VAR>minAx : Order.Frame.MinimalAxioms α<VAR>s : Set α<VAR>a : α<GOAL>a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
<VAR>α : Type u<VAR>minAx : Order.Frame.MinimalAxioms α<VAR>s : Set α<VAR>b : α<GOAL>sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b
<VAR>α : Type u<VAR>ι : Sort w<VAR>minAx : Order.Frame.MinimalAxioms α<VAR>f : ι → α<VAR>a : α<GOAL>(⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
<VAR>α : Type u<VAR>ι : Sort w<VAR>minAx : Order.Frame.MinimalAxioms α<VAR>a : α<VAR>f : ι → α<GOAL>a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : Order.Frame.MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j
<VAR>α : Type u<VAR>minAx : Order.Coframe.MinimalAxioms α<VAR>s : Set α<VAR>a : α<GOAL>a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b
<VAR>α : Type u<VAR>minAx : Order.Coframe.MinimalAxioms α<VAR>s : Set α<VAR>b : α<GOAL>sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b
<VAR>α : Type u<VAR>ι : Sort w<VAR>minAx : Order.Coframe.MinimalAxioms α<VAR>f : ι → α<VAR>a : α<GOAL>(⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a
<VAR>α : Type u<VAR>ι : Sort w<VAR>minAx : Order.Coframe.MinimalAxioms α<VAR>a : α<VAR>f : ι → α<GOAL>a ⊔ ⨅ i, f i = ⨅ i, a ⊔ f i
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : Order.Coframe.MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>a ⊔ ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a ⊔ f i j
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : CompletelyDistribLattice.MinimalAxioms α<VAR>f : (a : ι) → κ a → α<GOAL>let x := minAx.toCompleteLattice;
⨅ i, ⨆ j, f i j = ⨆ g, ⨅ i, f i (g i)
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : CompletelyDistribLattice.MinimalAxioms α<VAR>f : (i : ι) → κ i → α<GOAL>let x := minAx.toCompleteLattice;
⨆ i, ⨅ j, f i j = ⨅ g, ⨆ i, f i (g i)
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>CompletelyDistribLattice α<VAR>f : (a : ι) → κ a → α<GOAL>⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>CompletelyDistribLattice α<VAR>f : (a : ι) → κ a → α<GOAL>⨆ a, ⨅ b, f a b = ⨅ g, ⨆ a, f a (g a)
<VAR>α : Type u<VAR>Order.Frame α<VAR>s : Set α<VAR>a : α<GOAL>a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
<VAR>α : Type u<VAR>Order.Frame α<VAR>s : Set α<VAR>b : α<GOAL>sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b
<VAR>α : Type u<VAR>ι : Sort w<VAR>Order.Frame α<VAR>f : ι → α<VAR>a : α<GOAL>(⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
<VAR>α : Type u<VAR>ι : Sort w<VAR>Order.Frame α<VAR>a : α<VAR>f : ι → α<GOAL>a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>Order.Frame α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>(⨆ i, ⨆ j, f i j) ⊓ a = ⨆ i, ⨆ j, f i j ⊓ a
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>Order.Frame α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j
<VAR>α : Type u<VAR>Order.Frame α<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>f : ι → α<VAR>g : ι' → α<GOAL>(⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2
<VAR>α : Type u<VAR>Order.Frame α<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>f : ι → α<VAR>g : ι' → α<VAR>s : Set ι<VAR>t : Set ι'<GOAL>(⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2
<VAR>α : Type u<VAR>Order.Frame α<VAR>s t : Set α<GOAL>sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, p.1 ⊓ p.2
<VAR>α : Type u<VAR>ι : Sort w<VAR>Order.Frame α<VAR>a : α<VAR>f : ι → α<GOAL>Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a
<VAR>α : Type u<VAR>ι : Sort w<VAR>Order.Frame α<VAR>a : α<VAR>f : ι → α<GOAL>Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>Order.Frame α<VAR>a : α<VAR>f : (i : ι) → κ i → α<GOAL>Disjoint (⨆ i, ⨆ j, f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>Order.Frame α<VAR>a : α<VAR>f : (i : ι) → κ i → α<GOAL>Disjoint a (⨆ i, ⨆ j, f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)
<VAR>α : Type u<VAR>Order.Frame α<VAR>a : α<VAR>s : Set α<GOAL>Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a
<VAR>α : Type u<VAR>Order.Frame α<VAR>a : α<VAR>s : Set α<GOAL>Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b
<VAR>α : Type u<VAR>Order.Frame α<VAR>ι : Type u_1<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → α<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i
<VAR>α : Type u<VAR>Order.Frame α<VAR>ι : Type u_1<VAR>Preorder ι<VAR>IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)<VAR>f g : ι → α<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i
<VAR>α : Type u<VAR>Order.Coframe α<VAR>s : Set α<VAR>a : α<GOAL>a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b
<VAR>α : Type u<VAR>Order.Coframe α<VAR>s : Set α<VAR>b : α<GOAL>sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b
<VAR>α : Type u<VAR>ι : Sort w<VAR>Order.Coframe α<VAR>f : ι → α<VAR>a : α<GOAL>(⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a
<VAR>α : Type u<VAR>ι : Sort w<VAR>Order.Coframe α<VAR>a : α<VAR>f : ι → α<GOAL>a ⊔ ⨅ i, f i = ⨅ i, a ⊔ f i
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>Order.Coframe α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>(⨅ i, ⨅ j, f i j) ⊔ a = ⨅ i, ⨅ j, f i j ⊔ a
<VAR>α : Type u<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>Order.Coframe α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>a ⊔ ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a ⊔ f i j
<VAR>α : Type u<VAR>Order.Coframe α<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>f : ι → α<VAR>g : ι' → α<GOAL>(⨅ i, f i) ⊔ ⨅ i, g i = ⨅ i, f i.1 ⊔ g i.2
<VAR>α : Type u<VAR>Order.Coframe α<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>f : ι → α<VAR>g : ι' → α<VAR>s : Set ι<VAR>t : Set ι'<GOAL>(⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j = ⨅ p ∈ s ×ˢ t, f p.1 ⊔ g p.2
<VAR>α : Type u<VAR>Order.Coframe α<VAR>s t : Set α<GOAL>sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, p.1 ⊔ p.2