ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedAddCommGroup α<VAR>l : Filter β<VAR>u : β → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun x => -u x) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommGroup α<VAR>l : Filter β<VAR>u : β → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun x => (u x)⁻¹) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeSup α<VAR>f : Filter β<VAR>u v : β → α<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u → Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f v → Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => u a ⊔ v a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeSup α<VAR>f : Filter β<VAR>u v : β → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => u a ⊔ v a) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u ∧ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeInf α<VAR>f : Filter β<VAR>u v : β → α<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u → Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f v → Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f fun a => u a ⊓ v a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeInf α<VAR>f : Filter β<VAR>u v : β → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f fun a => u a ⊓ v a) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u ∧ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedAddCommGroup α<VAR>f : Filter β<VAR>u : β → α<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => |u a|) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u ∧ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>Filter.limsup u f = sInf {a | ∀ᶠ (n : β) in f, u n ≤ a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>Filter.liminf u f = sSup {a | ∀ᶠ (n : β) in f, a ≤ u n}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>p : β → Prop<GOAL>Filter.blimsup u f p = sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>p : β → Prop<GOAL>Filter.bliminf u f p = sSup {a | ∀ᶠ (x : β) in f, p x → a ≤ u x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>u : β → α<VAR>v : γ → β<VAR>f : Filter γ<GOAL>Filter.liminf (u ∘ v) f = Filter.liminf u (Filter.map v f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLattice α<VAR>u : β → α<VAR>v : γ → β<VAR>f : Filter γ<GOAL>Filter.limsup (u ∘ v) f = Filter.limsup u (Filter.map v f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>(Filter.blimsup u f fun x => True) = Filter.limsup u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>(Filter.bliminf u f fun x => True) = Filter.liminf u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>p : β → Prop<GOAL>Filter.blimsup u f p = Filter.limsup u (f ⊓ 𝓟 {x | p x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>p : β → Prop<GOAL>Filter.bliminf u f p = Filter.liminf u (f ⊓ 𝓟 {x | p x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>p : β → Prop<GOAL>Filter.blimsup u f p = Filter.limsup (u ∘ Subtype.val) (Filter.comap Subtype.val f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>p : β → Prop<GOAL>Filter.bliminf u f p = Filter.liminf (u ∘ Subtype.val) (Filter.comap Subtype.val f)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : Filter α<VAR>a : α<VAR>hf : Filter.IsCobounded (fun x x_1 => x ≤ x_1) f := by isBoundedDefault<VAR>h : ∀ᶠ (n : α) in f, n ≤ a<GOAL>f.limsSup ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : Filter α<VAR>a : α<VAR>hf : Filter.IsCobounded (fun x x_1 => x ≥ x_1) f := by isBoundedDefault<VAR>h : ∀ᶠ (n : α) in f, a ≤ n<GOAL>a ≤ f.limsInf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<VAR>hf : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>h : ∀ᶠ (n : β) in f, u n ≤ a<GOAL>Filter.limsup u f ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<VAR>hf : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>h : ∀ᶠ (n : β) in f, a ≤ u n<GOAL>a ≤ Filter.liminf u f
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : Filter α<VAR>a : α<VAR>hf : Filter.IsBounded (fun x x_1 => x ≤ x_1) f := by isBoundedDefault<VAR>h : ∀ (b : α), (∀ᶠ (n : α) in f, n ≤ b) → a ≤ b<GOAL>a ≤ f.limsSup
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : Filter α<VAR>a : α<VAR>hf : Filter.IsBounded (fun x x_1 => x ≥ x_1) f := by isBoundedDefault<VAR>h : ∀ (b : α), (∀ᶠ (n : α) in f, b ≤ n) → b ≤ a<GOAL>f.limsInf ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>h : ∀ (b : α), (∀ᶠ (n : β) in f, u n ≤ b) → a ≤ b<GOAL>a ≤ Filter.limsup u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>h : ∀ (b : α), (∀ᶠ (n : β) in f, b ≤ u n) → b ≤ a<GOAL>Filter.liminf u f ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : Filter α<VAR>f.NeBot<VAR>h₁ : Filter.IsBounded (fun x x_1 => x ≤ x_1) f := by isBoundedDefault<VAR>h₂ : Filter.IsBounded (fun x x_1 => x ≥ x_1) f := by isBoundedDefault<GOAL>f.limsInf ≤ f.limsSup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>f.NeBot<VAR>u : β → α<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 u := by isBoundedDefault<GOAL>Filter.liminf u f ≤ Filter.limsup u f
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f g : Filter α<VAR>hf : Filter.IsCobounded (fun x x_1 => x ≤ x_1) f := by isBoundedDefault<VAR>hg : Filter.IsBounded (fun x x_1 => x ≤ x_1) g := by isBoundedDefault<VAR>h : ∀ (a : α), (∀ᶠ (n : α) in g, n ≤ a) → ∀ᶠ (n : α) in f, n ≤ a<GOAL>f.limsSup ≤ g.limsSup
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f g : Filter α<VAR>hf : Filter.IsBounded (fun x x_1 => x ≥ x_1) f := by isBoundedDefault<VAR>hg : Filter.IsCobounded (fun x x_1 => x ≥ x_1) g := by isBoundedDefault<VAR>h : ∀ (a : α), (∀ᶠ (n : α) in f, a ≤ n) → ∀ᶠ (n : α) in g, a ≤ n<GOAL>f.limsInf ≤ g.limsInf
<VAR>β : Type u_2<VAR>α : Type u_6<VAR>ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>u v : α → β<VAR>h : u ≤ᶠ[f] v<VAR>hu : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>hv : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f v := by isBoundedDefault<GOAL>Filter.limsup u f ≤ Filter.limsup v f
<VAR>β : Type u_2<VAR>α : Type u_6<VAR>ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>u v : α → β<VAR>h : ∀ᶠ (a : α) in f, u a ≤ v a<VAR>hu : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>hv : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f v := by isBoundedDefault<GOAL>Filter.liminf u f ≤ Filter.liminf v f
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f g : Filter α<VAR>h : f ≤ g<VAR>hf : Filter.IsCobounded (fun x x_1 => x ≤ x_1) f := by isBoundedDefault<VAR>hg : Filter.IsBounded (fun x x_1 => x ≤ x_1) g := by isBoundedDefault<GOAL>f.limsSup ≤ g.limsSup
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f g : Filter α<VAR>h : g ≤ f<VAR>hf : Filter.IsBounded (fun x x_1 => x ≥ x_1) f := by isBoundedDefault<VAR>hg : Filter.IsCobounded (fun x x_1 => x ≥ x_1) g := by isBoundedDefault<GOAL>f.limsInf ≤ g.limsInf
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLattice β<VAR>f g : Filter α<VAR>h : f ≤ g<VAR>u : α → β<VAR>hf : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>hg : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) g u := by isBoundedDefault<GOAL>Filter.limsup u f ≤ Filter.limsup u g
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ConditionallyCompleteLattice β<VAR>f g : Filter α<VAR>h : g ≤ f<VAR>u : α → β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<VAR>hg : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) g u := by isBoundedDefault<GOAL>Filter.liminf u f ≤ Filter.liminf u g
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>h : BddAbove s<VAR>hs : s.Nonempty<GOAL>(𝓟 s).limsSup = sSup s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>h : BddBelow s<VAR>hs : s.Nonempty<GOAL>(𝓟 s).limsInf = sInf s
<VAR>β : Type u_2<VAR>α : Type u_6<VAR>ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>u v : α → β<VAR>h : ∀ᶠ (a : α) in f, u a = v a<GOAL>Filter.limsup u f = Filter.limsup v f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u v : β → α<VAR>p : β → Prop<VAR>h : ∀ᶠ (a : β) in f, p a → u a = v a<GOAL>Filter.blimsup u f p = Filter.blimsup v f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u v : β → α<VAR>p : β → Prop<VAR>h : ∀ᶠ (a : β) in f, p a → u a = v a<GOAL>Filter.bliminf u f p = Filter.bliminf v f p
<VAR>β : Type u_2<VAR>α : Type u_6<VAR>ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>u v : α → β<VAR>h : ∀ᶠ (a : α) in f, u a = v a<GOAL>Filter.liminf u f = Filter.liminf v f
<VAR>β : Type u_2<VAR>α : Type u_6<VAR>ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>f.NeBot<VAR>b : β<GOAL>Filter.limsup (fun x => b) f = b
<VAR>β : Type u_2<VAR>α : Type u_6<VAR>ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>f.NeBot<VAR>b : β<GOAL>Filter.liminf (fun x => b) f = b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>f : ι → α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasBasis p s<GOAL>Filter.liminf f v = sSup (⋃ j, ⋂ i, Set.Iic (f ↑i))
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ConditionallyCompleteLattice α<VAR>f : ι → α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasBasis p s<VAR>i : ι'<VAR>hi : p i<VAR>h'i : s i = ∅<GOAL>Filter.liminf f v = sSup Set.univ
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>f : ι → α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasBasis p s<GOAL>Filter.limsup f v = sInf (⋃ j, ⋂ i, Set.Ici (f ↑i))
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ConditionallyCompleteLattice α<VAR>f : ι → α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasBasis p s<VAR>i : ι'<VAR>hi : p i<VAR>h'i : s i = ∅<GOAL>Filter.limsup f v = sInf Set.univ
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : ℕ → α<VAR>k : ℕ<GOAL>Filter.liminf (fun i => f (i + k)) Filter.atTop = Filter.liminf f Filter.atTop
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : ℕ → α<VAR>k : ℕ<GOAL>Filter.limsup (fun i => f (i + k)) Filter.atTop = Filter.limsup f Filter.atTop
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>⊥.limsSup = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<GOAL>Filter.limsup f ⊥ = ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>⊥.limsInf = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : β → α<GOAL>Filter.liminf f ⊥ = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>⊤.limsSup = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>⊤.limsInf = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>(Filter.blimsup u f fun x => False) = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>(Filter.bliminf u f fun x => False) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<GOAL>Filter.limsup (fun x => ⊥) f = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<GOAL>Filter.liminf (fun x => ⊤) f = ⊤
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Sort u_6<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : Filter α<VAR>h : f.HasBasis p s<GOAL>f.limsSup = ⨅ i, ⨅ (_ : p i), sSup (s i)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : Filter α<VAR>h : f.HasBasis p s<GOAL>f.limsInf = ⨆ i, ⨆ (_ : p i), sInf (s i)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : Filter α<GOAL>f.limsSup = ⨅ s ∈ f, sSup s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : Filter α<GOAL>f.limsInf = ⨆ s ∈ f, sInf s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>Filter.limsup u f ≤ ⨆ n, u n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>⨅ n, u n ≤ Filter.liminf u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>Filter.limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<GOAL>Filter.limsup u Filter.atTop = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<GOAL>Filter.limsup u Filter.atTop = ⨅ n, ⨆ i, u (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>s : ι → Set β<VAR>f : Filter β<VAR>u : β → α<VAR>h : f.HasBasis p s<GOAL>Filter.limsup u f = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, u a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)<GOAL>Filter.blimsup u f p = Filter.blimsup u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ᶠ (x : β) in f, u x ≠ ⊤ → (p x ↔ q x)<GOAL>Filter.bliminf u f p = Filter.bliminf u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>s : ι → Set β<VAR>f : Filter β<VAR>u : β → α<VAR>hf : f.HasBasis p s<VAR>q : β → Prop<GOAL>Filter.blimsup u f q = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<GOAL>Filter.blimsup u f p = ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : ℕ → Prop<VAR>u : ℕ → α<GOAL>Filter.blimsup u Filter.atTop p = ⨅ i, ⨆ j, ⨆ (_ : p j ∧ i ≤ j), u j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>Filter.liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<GOAL>Filter.liminf u Filter.atTop = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), u i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<GOAL>Filter.liminf u Filter.atTop = ⨆ n, ⨅ i, u (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>CompleteLattice α<VAR>p : ι → Prop<VAR>s : ι → Set β<VAR>f : Filter β<VAR>u : β → α<VAR>h : f.HasBasis p s<GOAL>Filter.liminf u f = ⨆ i, ⨆ (_ : p i), ⨅ a ∈ s i, u a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<GOAL>Filter.bliminf u f p = ⨆ s ∈ f, ⨅ b, ⨅ (_ : p b ∧ b ∈ s), u b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : ℕ → Prop<VAR>u : ℕ → α<GOAL>Filter.bliminf u Filter.atTop p = ⨆ i, ⨅ j, ⨅ (_ : p j ∧ i ≤ j), u j
<VAR>ι : Type u_6<VAR>R : Type u_7<VAR>F : Filter ι<VAR>CompleteLattice R<VAR>a : ι → R<GOAL>Filter.limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)
<VAR>ι : Type u_6<VAR>R : Type u_7<VAR>F : Filter ι<VAR>CompleteLattice R<VAR>a : ι → R<GOAL>Filter.liminf a F = sSup ((fun I => sInf (a '' I)) '' F.sets)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>CompleteLattice β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h : ∃ᶠ (a : α) in f, u a ≤ x<GOAL>Filter.liminf u f ≤ x
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>CompleteLattice β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h : ∃ᶠ (a : α) in f, x ≤ u a<GOAL>x ≤ Filter.limsup u f
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>f (Filter.limsup (fun n => (⇑f)^[n] a) Filter.atTop) = Filter.limsup (fun n => (⇑f)^[n] a) Filter.atTop
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>f (Filter.liminf (fun n => (⇑f)^[n] a) Filter.atTop) = Filter.liminf (fun n => (⇑f)^[n] a) Filter.atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ (x : β), p x → q x<GOAL>Filter.blimsup u f p ≤ Filter.blimsup u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ (x : β), p x → q x<GOAL>Filter.bliminf u f q ≤ Filter.bliminf u f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u v : β → α<VAR>h : ∀ᶠ (x : β) in f, p x → u x ≤ v x<GOAL>Filter.blimsup u f p ≤ Filter.blimsup v f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u v : β → α<VAR>h : ∀ (x : β), p x → u x ≤ v x<GOAL>Filter.blimsup u f p ≤ Filter.blimsup v f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u v : β → α<VAR>h : ∀ᶠ (x : β) in f, p x → u x ≤ v x<GOAL>Filter.bliminf u f p ≤ Filter.bliminf v f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u v : β → α<VAR>h : ∀ (x : β), p x → u x ≤ v x<GOAL>Filter.bliminf u f p ≤ Filter.bliminf v f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f g : Filter β<VAR>p : β → Prop<VAR>u : β → α<VAR>h : f ≤ g<GOAL>Filter.bliminf u g p ≤ Filter.bliminf u f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f g : Filter β<VAR>p : β → Prop<VAR>u : β → α<VAR>h : f ≤ g<GOAL>Filter.blimsup u f p ≤ Filter.blimsup u g p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(Filter.blimsup u f fun x => p x ∧ q x) ≤ Filter.blimsup u f p ⊓ Filter.blimsup u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(Filter.blimsup u f fun x => p x ∧ q x) ≤ Filter.blimsup u f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(Filter.blimsup u f fun x => p x ∧ q x) ≤ Filter.blimsup u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>Filter.bliminf u f p ⊔ Filter.bliminf u f q ≤ Filter.bliminf u f fun x => p x ∧ q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>Filter.bliminf u f p ≤ Filter.bliminf u f fun x => p x ∧ q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>Filter.bliminf u f q ≤ Filter.bliminf u f fun x => p x ∧ q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>Filter.blimsup u f p ⊔ Filter.blimsup u f q ≤ Filter.blimsup u f fun x => p x ∨ q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>Filter.blimsup u f p ≤ Filter.blimsup u f fun x => p x ∨ q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>Filter.blimsup u f q ≤ Filter.blimsup u f fun x => p x ∨ q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(Filter.bliminf u f fun x => p x ∨ q x) ≤ Filter.bliminf u f p ⊓ Filter.bliminf u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(Filter.bliminf u f fun x => p x ∨ q x) ≤ Filter.bliminf u f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(Filter.bliminf u f fun x => p x ∨ q x) ≤ Filter.bliminf u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<VAR>CompleteLattice γ<VAR>e : α ≃o γ<GOAL>e (Filter.blimsup u f p) = Filter.blimsup (⇑e ∘ u) f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<VAR>CompleteLattice γ<VAR>e : α ≃o γ<GOAL>e (Filter.bliminf u f p) = Filter.bliminf (⇑e ∘ u) f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<VAR>CompleteLattice γ<VAR>g : sSupHom α γ<GOAL>g (Filter.blimsup u f p) ≤ Filter.blimsup (⇑g ∘ u) f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<VAR>CompleteLattice γ<VAR>g : sInfHom α γ<GOAL>Filter.bliminf (⇑g ∘ u) f p ≤ g (Filter.bliminf u f p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>g : Filter β<GOAL>Filter.limsup u (f ⊔ g) = Filter.limsup u f ⊔ Filter.limsup u g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>g : Filter β<GOAL>Filter.liminf u (f ⊔ g) = Filter.liminf u f ⊓ Filter.liminf u g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(Filter.blimsup u f fun x => p x ∨ q x) = Filter.blimsup u f p ⊔ Filter.blimsup u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(Filter.bliminf u f fun x => p x ∨ q x) = Filter.bliminf u f p ⊓ Filter.bliminf u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<GOAL>(Filter.blimsup u f p ⊔ Filter.blimsup u f fun x => ¬p x) = Filter.limsup u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<GOAL>(Filter.bliminf u f p ⊓ Filter.bliminf u f fun x => ¬p x) = Filter.liminf u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<GOAL>(Filter.blimsup u f fun x => ¬p x) ⊔ Filter.blimsup u f p = Filter.limsup u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<GOAL>(Filter.bliminf u f fun x => ¬p x) ⊓ Filter.bliminf u f p = Filter.liminf u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set β<VAR>DecidablePred fun x => x ∈ s<VAR>v : β → α<GOAL>Filter.limsup (s.piecewise u v) f = (Filter.blimsup u f fun x => x ∈ s) ⊔ Filter.blimsup v f fun x => x ∉ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set β<VAR>DecidablePred fun x => x ∈ s<VAR>v : β → α<GOAL>Filter.liminf (s.piecewise u v) f = (Filter.bliminf u f fun x => x ∈ s) ⊓ Filter.bliminf v f fun x => x ∉ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>f.NeBot<VAR>a : α<GOAL>a ⊔ Filter.limsup u f = Filter.limsup (fun x => a ⊔ u x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>f.NeBot<VAR>a : α<GOAL>a ⊓ Filter.liminf u f = Filter.liminf (fun x => a ⊓ u x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>a ⊔ Filter.liminf u f = Filter.liminf (fun x => a ⊔ u x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteDistribLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>a ⊓ Filter.limsup u f = Filter.limsup (fun x => a ⊓ u x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<GOAL>(Filter.limsup u f)ᶜ = Filter.liminf (compl ∘ u) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<GOAL>(Filter.liminf u f)ᶜ = Filter.limsup (compl ∘ u) f