ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ 0 < r
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ 0 < r
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ 0 < r
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atTop
<VAR>α : Type u_3<VAR>LinearOrderedSemifield α<VAR>c : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hc : 0 < c<GOAL>Filter.Tendsto (fun x => c * x ^ n) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>LinearOrderedSemifield α<VAR>c : α<VAR>n : ℕ<GOAL>Filter.Tendsto (fun x => c * x ^ n) Filter.atTop Filter.atTop ↔ n ≠ 0 ∧ 0 < c
<VAR>α : Type u_3<VAR>LinearOrderedSemifield α<VAR>n : ℤ<VAR>hn : 0 < n<GOAL>Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ 0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ 0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ 0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ 0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ 0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ 0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ r < 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ r < 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ r < 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ 0 < r
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ 0 < r
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ 0 < r
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ r < 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ r < 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>l.NeBot<VAR>h : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ r < 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop
<VAR>α : Type u_3<VAR>LinearOrderedField α<VAR>c : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hc : c < 0<GOAL>Filter.Tendsto (fun x => c * x ^ n) Filter.atTop Filter.atBot
<VAR>α : Type u_3<VAR>LinearOrderedField α<VAR>c : α<VAR>n : ℕ<GOAL>Filter.Tendsto (fun x => c * x ^ n) Filter.atTop Filter.atBot ↔ n ≠ 0 ∧ c < 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>f : α → β<VAR>l : Filter β<GOAL>Filter.Tendsto f Filter.atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>f : α → β<VAR>l : Filter β<GOAL>Filter.Tendsto f Filter.atBot l ↔ ∀ s ∈ l, ∃ a, ∀ b ≤ a, f b ∈ s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>f : β → α<VAR>s : Set α<GOAL>Filter.Tendsto f Filter.atTop (𝓟 s) ↔ ∃ N, ∀ n ≥ N, f n ∈ s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty β<VAR>SemilatticeInf β<VAR>f : β → α<VAR>s : Set α<GOAL>Filter.Tendsto f Filter.atBot (𝓟 s) ↔ ∃ N, ∀ n ≤ N, f n ∈ s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>Preorder β<VAR>f : α → β<GOAL>Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ i, ∀ (a : α), i ≤ a → b ≤ f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>Preorder β<VAR>f : α → β<GOAL>Filter.Tendsto f Filter.atTop Filter.atBot ↔ ∀ (b : β), ∃ i, ∀ (a : α), i ≤ a → f a ≤ b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>Preorder β<VAR>f : α → β<GOAL>Filter.Tendsto f Filter.atBot Filter.atTop ↔ ∀ (b : β), ∃ i, ∀ a ≤ i, b ≤ f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>Preorder β<VAR>f : α → β<GOAL>Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ i, ∀ a ≤ i, f a ≤ b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>h : ∀ (b : β), ∃ a, b ≤ f a<GOAL>Filter.Tendsto f Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>h : ∀ (b : β), ∃ a, f a ≤ b<GOAL>Filter.Tendsto f Filter.atTop Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>h : ∀ (b : β), ∃ a, f a ≤ b<GOAL>Filter.Tendsto f Filter.atBot Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>h : ∀ (b : β), ∃ a, b ≤ f a<GOAL>Filter.Tendsto f Filter.atBot Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ a, b ≤ f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Filter.Tendsto f Filter.atTop Filter.atBot ↔ ∀ (b : β), ∃ a, f a ≤ b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ a, f a ≤ b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Filter.Tendsto f Filter.atBot Filter.atTop ↔ ∀ (b : β), ∃ a, b ≤ f a
<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder β<VAR>Preorder γ<VAR>e : β → γ<VAR>hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂<VAR>hu : ∀ (c : γ), ∃ b, c ≤ e b<GOAL>Filter.comap e Filter.atTop = Filter.atTop
<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder β<VAR>Preorder γ<VAR>e : β → γ<VAR>hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂<VAR>hu : ∀ (c : γ), ∃ b, e b ≤ c<GOAL>Filter.comap e Filter.atBot = Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>e : β → γ<VAR>l : Filter α<VAR>hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂<VAR>hu : ∀ (c : γ), ∃ b, c ≤ e b<GOAL>Filter.Tendsto (e ∘ f) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>e : β → γ<VAR>l : Filter α<VAR>hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂<VAR>hu : ∀ (c : γ), ∃ b, e b ≤ c<GOAL>Filter.Tendsto (e ∘ f) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
<GOAL>Filter.Tendsto Finset.range Filter.atTop Filter.atTop
<VAR>α : Type u_3<GOAL>Filter.atTop = ⨅ x, 𝓟 (Set.Ici {x})
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>f : β → Finset α<VAR>h : Monotone f<VAR>h' : ∀ (x : α), ∃ n, x ∈ f n<GOAL>Filter.Tendsto f Filter.atTop Filter.atTop
<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>DecidableEq β<VAR>i : β → γ<VAR>j : γ → β<VAR>h : Function.LeftInverse j i<GOAL>Filter.Tendsto (Finset.image j) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Filter.Tendsto (fun s => s.preimage f ⋯) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<GOAL>Filter.atTop ×ˢ Filter.atTop = Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<GOAL>Filter.atBot ×ˢ Filter.atBot = Filter.atBot
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>Preorder β₁<VAR>Preorder β₂<VAR>u₁ : β₁ → α₁<VAR>u₂ : β₂ → α₂<GOAL>Filter.map u₁ Filter.atTop ×ˢ Filter.map u₂ Filter.atTop = Filter.map (Prod.map u₁ u₂) Filter.atTop
<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>Preorder β₁<VAR>Preorder β₂<VAR>u₁ : β₁ → α₁<VAR>u₂ : β₂ → α₂<GOAL>Filter.map u₁ Filter.atBot ×ˢ Filter.map u₂ Filter.atBot = Filter.map (Prod.map u₁ u₂) Filter.atBot
<VAR>α : Type u_3<VAR>F : Filter α<VAR>V : ℕ → Set α<VAR>h : ∀ (n : ℕ), V n ∈ F<VAR>u : ℕ → α<VAR>hu : Filter.Tendsto u Filter.atTop F<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), u (φ n) ∈ V n
<VAR>α : Type u_3<VAR>SemilatticeInf α<GOAL>Filter.Tendsto (fun a => (a, a)) Filter.atBot Filter.atBot
<VAR>α : Type u_3<VAR>SemilatticeSup α<GOAL>Filter.Tendsto (fun a => (a, a)) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>SemilatticeInf γ<VAR>F : Filter α<VAR>G : Filter β<VAR>f : α → γ<VAR>g : β → γ<VAR>hf : Filter.Tendsto f F Filter.atBot<VAR>hg : Filter.Tendsto g G Filter.atBot<GOAL>Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>SemilatticeSup γ<VAR>F : Filter α<VAR>G : Filter β<VAR>f : α → γ<VAR>g : β → γ<VAR>hf : Filter.Tendsto f F Filter.atTop<VAR>hg : Filter.Tendsto g G Filter.atTop<GOAL>Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atTop
<VAR>α : Type u_3<VAR>γ : Type u_5<VAR>SemilatticeInf α<VAR>SemilatticeInf γ<VAR>f g : α → γ<VAR>hf : Filter.Tendsto f Filter.atBot Filter.atBot<VAR>hg : Filter.Tendsto g Filter.atBot Filter.atBot<GOAL>Filter.Tendsto (Prod.map f g) Filter.atBot Filter.atBot
<VAR>α : Type u_3<VAR>γ : Type u_5<VAR>SemilatticeSup α<VAR>SemilatticeSup γ<VAR>f g : α → γ<VAR>hf : Filter.Tendsto f Filter.atTop Filter.atTop<VAR>hg : Filter.Tendsto g Filter.atTop Filter.atTop<GOAL>Filter.Tendsto (Prod.map f g) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>p : α × α → Prop<GOAL>(∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>p : α × α → Prop<GOAL>(∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ a, ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>p : α × α → Prop<GOAL>(∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>p : α × α → Prop<GOAL>(∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>p : α × β → Prop<VAR>hp : ∀ᶠ (x : α × β) in Filter.atTop, p x<GOAL>∀ᶠ (k : α) in Filter.atTop, ∀ᶠ (l : β) in Filter.atTop, p (k, l)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>p : α × β → Prop<VAR>hp : ∀ᶠ (x : α × β) in Filter.atBot, p x<GOAL>∀ᶠ (k : α) in Filter.atBot, ∀ᶠ (l : β) in Filter.atBot, p (k, l)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α → β<VAR>g : β → α<VAR>b' : β<VAR>hf : Monotone f<VAR>gc : ∀ (a : α), ∀ b ≥ b', f a ≤ b ↔ a ≤ g b<VAR>hgi : ∀ b ≥ b', b ≤ f (g b)<GOAL>Filter.map f Filter.atTop = Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α → β<VAR>g : β → α<VAR>b' : β<VAR>hf : Monotone f<VAR>gc : ∀ (a : α), ∀ b ≤ b', b ≤ f a ↔ g b ≤ a<VAR>hgi : ∀ b ≤ b', f (g b) ≤ b<GOAL>Filter.map f Filter.atBot = Filter.atBot
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>a : α<VAR>s : Set α<VAR>h : Set.Ici a ⊆ s<GOAL>Filter.map Subtype.val Filter.atTop = Filter.atTop
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>a : α<GOAL>Filter.map Subtype.val Filter.atTop = Filter.atTop
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Filter.map Subtype.val Filter.atTop = Filter.atTop
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>a : α<GOAL>Filter.atTop = Filter.comap Subtype.val Filter.atTop
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>NoMinOrder α<VAR>a : α<GOAL>Filter.map Subtype.val Filter.atBot = Filter.atBot
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>a : α<GOAL>Filter.atBot = Filter.comap Subtype.val Filter.atBot
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>a : α<GOAL>Filter.map Subtype.val Filter.atBot = Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>a : α<VAR>f : β → ↑(Set.Ioi a)<VAR>l : Filter β<GOAL>Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun x => ↑(f x)) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>a : α<VAR>f : β → ↑(Set.Iio a)<VAR>l : Filter β<GOAL>Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun x => ↑(f x)) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>a : α<VAR>f : β → ↑(Set.Ici a)<VAR>l : Filter β<GOAL>Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun x => ↑(f x)) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>a : α<VAR>f : β → ↑(Set.Iic a)<VAR>l : Filter β<GOAL>Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun x => ↑(f x)) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>NoMaxOrder α<VAR>a : α<VAR>f : α → β<VAR>l : Filter β<GOAL>Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>a : α<VAR>f : α → β<VAR>l : Filter β<GOAL>Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>NoMinOrder α<VAR>a : α<VAR>f : α → β<VAR>l : Filter β<GOAL>Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f Filter.atBot l
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>a : α<VAR>f : α → β<VAR>l : Filter β<GOAL>Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f Filter.atBot l
<VAR>k : ℕ<GOAL>Filter.map (fun a => a + k) Filter.atTop = Filter.atTop
<VAR>k : ℕ<GOAL>Filter.map (fun a => a - k) Filter.atTop = Filter.atTop
<VAR>k : ℕ<GOAL>Filter.Tendsto (fun a => a + k) Filter.atTop Filter.atTop
<VAR>k : ℕ<GOAL>Filter.Tendsto (fun a => a - k) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>f : ℕ → α<VAR>l : Filter α<VAR>k : ℕ<GOAL>Filter.Tendsto (fun n => f (n + k)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
<VAR>k : ℕ<VAR>hk : 0 < k<GOAL>Filter.map (fun a => a / k) Filter.atTop = Filter.atTop
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder ι<VAR>LinearOrder α<VAR>u : ι → α<VAR>h : Monotone u<VAR>H : ¬BddAbove (Set.range u)<GOAL>Filter.Tendsto u Filter.atTop Filter.atTop
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder ι<VAR>LinearOrder α<VAR>u : ι → α<VAR>h : Monotone u<VAR>H : ¬BddBelow (Set.range u)<GOAL>Filter.Tendsto u Filter.atBot Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>Preorder β<VAR>NoMaxOrder β<VAR>f : α → β<VAR>h : Filter.Tendsto f Filter.atTop Filter.atTop<GOAL>¬BddAbove (Set.range f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>Preorder β<VAR>NoMinOrder β<VAR>f : α → β<VAR>h : Filter.Tendsto f Filter.atTop Filter.atBot<GOAL>¬BddBelow (Set.range f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>Preorder β<VAR>NoMaxOrder β<VAR>f : α → β<VAR>h : Filter.Tendsto f Filter.atBot Filter.atTop<GOAL>¬BddAbove (Set.range f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>Preorder β<VAR>NoMinOrder β<VAR>f : α → β<VAR>h : Filter.Tendsto f Filter.atBot Filter.atBot<GOAL>¬BddBelow (Set.range f)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder ι<VAR>Preorder α<VAR>l : Filter ι<VAR>u : ι → α<VAR>h : Monotone u<VAR>l.NeBot<VAR>hu : Filter.Tendsto u l Filter.atTop<GOAL>Filter.Tendsto u Filter.atTop Filter.atTop
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder ι<VAR>Preorder α<VAR>l : Filter ι<VAR>u : ι → α<VAR>h : Monotone u<VAR>l.NeBot<VAR>hu : Filter.Tendsto u l Filter.atBot<GOAL>Filter.Tendsto u Filter.atBot Filter.atBot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Preorder ι<VAR>Preorder α<VAR>u : ι → α<VAR>φ : ι' → ι<VAR>h : Monotone u<VAR>l : Filter ι'<VAR>l.NeBot<VAR>H : Filter.Tendsto (u ∘ φ) l Filter.atTop<GOAL>Filter.Tendsto u Filter.atTop Filter.atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>Preorder ι<VAR>Preorder α<VAR>u : ι → α<VAR>φ : ι' → ι<VAR>h : Monotone u<VAR>l : Filter ι'<VAR>l.NeBot<VAR>H : Filter.Tendsto (u ∘ φ) l Filter.atBot<GOAL>Filter.Tendsto u Filter.atBot Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid α<VAR>f : β → α<VAR>g : γ → α<VAR>h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b<GOAL>Filter.map (fun s => ∏ b ∈ s, f b) Filter.atTop ≤ Filter.map (fun s => ∏ x ∈ s, g x) Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid α<VAR>f : β → α<VAR>g : γ → α<VAR>h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b<GOAL>Filter.map (fun s => ∑ b ∈ s, f b) Filter.atTop ≤ Filter.map (fun s => ∑ x ∈ s, g x) Filter.atTop
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder ι<VAR>l : Filter α<VAR>s : ι → Set α<VAR>hl : l.HasAntitoneBasis s<VAR>t : Set α<VAR>ht : t ∈ l<GOAL>∀ᶠ (i : ι) in Filter.atTop, s i ⊆ t
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder ι<VAR>l : Filter α<VAR>s : ι → Set α<VAR>hl : l.HasAntitoneBasis s<VAR>φ : ι → α<VAR>h : ∀ (i : ι), φ i ∈ s i<GOAL>Filter.Tendsto φ Filter.atTop l
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>Preorder ι'<VAR>l : Filter α<VAR>s : ι' → Set α<VAR>hs : l.HasAntitoneBasis s<VAR>φ : ι → ι'<VAR>φ_mono : Monotone φ<VAR>hφ : Filter.Tendsto φ Filter.atTop Filter.atTop<GOAL>l.HasAntitoneBasis (s ∘ φ)
<VAR>α : Type u_3<VAR>l : Filter α<VAR>s : ℕ → Set α<VAR>hs : l.HasAntitoneBasis s<VAR>φ : ℕ → ℕ<VAR>hφ : StrictMono φ<GOAL>l.HasAntitoneBasis (s ∘ φ)
<VAR>α : Type u_3<VAR>f : Filter α<VAR>s : ℕ → Set α<VAR>hs : f.HasAntitoneBasis s<VAR>r : ℕ → ℕ → Prop<VAR>hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, r m n<GOAL>∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)
<VAR>α : Type u_3<VAR>f : Filter α<VAR>f.IsCountablyGenerated<VAR>f.NeBot<GOAL>∃ x, Filter.Tendsto x Filter.atTop f
<VAR>α : Type u_6<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>Filter.atTop.IsCountablyGenerated<GOAL>∃ xs, Monotone xs ∧ Filter.Tendsto xs Filter.atTop Filter.atTop
<VAR>α : Type u_6<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>h2 : Filter.atBot.IsCountablyGenerated<GOAL>∃ xs, Antitone xs ∧ Filter.Tendsto xs Filter.atTop Filter.atBot