ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : α<GOAL>IsComplemented a → IsComplemented b → IsComplemented (a ⊔ b)
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : α<GOAL>IsComplemented a → IsComplemented b → IsComplemented (a ⊓ b)
<VAR>α : Type u_2<VAR>Lattice α<VAR>BoundedOrder α<VAR>self : ComplementedLattice α<VAR>a : α<GOAL>∃ b, IsCompl a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>Function.Injective Subtype.val
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>a b : Complementeds α<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>a b : Complementeds α<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>a b : Complementeds α<GOAL>↑a < ↑b ↔ a < b
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>↑⊥ = ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>↑⊤ = ⊤
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>⟨⊥, ⋯⟩ = ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>⟨⊤, ⋯⟩ = ⊤
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : Complementeds α<GOAL>↑(a ⊔ b) = ↑a ⊔ ↑b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : Complementeds α<GOAL>↑(a ⊓ b) = ↑a ⊓ ↑b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : α<VAR>ha : IsComplemented a<VAR>hb : IsComplemented b<GOAL>⟨a, ha⟩ ⊔ ⟨b, hb⟩ = ⟨a ⊔ b, ⋯⟩
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : α<VAR>ha : IsComplemented a<VAR>hb : IsComplemented b<GOAL>⟨a, ha⟩ ⊓ ⟨b, hb⟩ = ⟨a ⊓ b, ⋯⟩
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : Complementeds α<GOAL>Disjoint ↑a ↑b ↔ Disjoint a b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : Complementeds α<GOAL>Codisjoint ↑a ↑b ↔ Codisjoint a b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b : Complementeds α<GOAL>IsCompl ↑a ↑b ↔ IsCompl a b
<VAR>α : Type u_2<VAR>Zero α<VAR>s : Set α<GOAL>s ∈ 0 ↔ 0 ∈ s
<VAR>α : Type u_2<VAR>One α<VAR>s : Set α<GOAL>s ∈ 1 ↔ 1 ∈ s
<VAR>α : Type u_2<VAR>One α<GOAL>1 ∈ 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>0 ∈ 0
<VAR>α : Type u_2<VAR>Zero α<GOAL>pure 0 = 0
<VAR>α : Type u_2<VAR>One α<GOAL>pure 1 = 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>𝓟 0 = 0
<VAR>α : Type u_2<VAR>One α<GOAL>𝓟 1 = 1
<VAR>α : Type u_2<VAR>One α<GOAL>Filter.NeBot 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>Filter.NeBot 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>f : α → β<GOAL>Filter.map f 0 = pure (f 0)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>f : α → β<GOAL>Filter.map f 1 = pure (f 1)
<VAR>α : Type u_2<VAR>One α<VAR>f : Filter α<GOAL>f ≤ 1 ↔ 1 ∈ f
<VAR>α : Type u_2<VAR>Zero α<VAR>f : Filter α<GOAL>f ≤ 0 ↔ 0 ∈ f
<VAR>α : Type u_2<VAR>One α<VAR>f : Filter α<VAR>h : f.NeBot<GOAL>f ≤ 1 ↔ f = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>f : Filter α<VAR>h : f.NeBot<GOAL>f ≤ 0 ↔ f = 0
<VAR>α : Type u_2<VAR>One α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in 1, p x) ↔ p 1
<VAR>α : Type u_2<VAR>Zero α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in 0, p x) ↔ p 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>a : Filter β<VAR>f : β → α<GOAL>Filter.Tendsto f a 1 ↔ ∀ᶠ (x : β) in a, f x = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>a : Filter β<VAR>f : β → α<GOAL>Filter.Tendsto f a 0 ↔ ∀ᶠ (x : β) in a, f x = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<GOAL>0 ×ˢ 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>One β<GOAL>1 ×ˢ 1 = 1
<VAR>α : Type u_2<VAR>One α<GOAL>⇑Filter.pureOneHom = pure
<VAR>α : Type u_2<VAR>Zero α<GOAL>⇑Filter.pureZeroHom = pure
<VAR>α : Type u_2<VAR>Zero α<VAR>a : α<GOAL>Filter.pureZeroHom a = pure a
<VAR>α : Type u_2<VAR>One α<VAR>a : α<GOAL>Filter.pureOneHom a = pure a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>FunLike F α β<VAR>ZeroHomClass F α β<VAR>φ : F<GOAL>Filter.map (⇑φ) 0 = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>One β<VAR>FunLike F α β<VAR>OneHomClass F α β<VAR>φ : F<GOAL>Filter.map (⇑φ) 1 = 1
<VAR>α : Type u_2<VAR>Inv α<VAR>f : Filter α<GOAL>Filter.map Inv.inv f = f⁻¹
<VAR>α : Type u_2<VAR>Neg α<VAR>f : Filter α<GOAL>Filter.map Neg.neg f = -f
<VAR>α : Type u_2<VAR>Inv α<VAR>f : Filter α<VAR>s : Set α<GOAL>s ∈ f⁻¹ ↔ Inv.inv ⁻¹' s ∈ f
<VAR>α : Type u_2<VAR>Neg α<VAR>f : Filter α<VAR>s : Set α<GOAL>s ∈ -f ↔ Neg.neg ⁻¹' s ∈ f
<VAR>α : Type u_2<VAR>Neg α<VAR>f g : Filter α<VAR>hf : f ≤ g<GOAL>-f ≤ -g
<VAR>α : Type u_2<VAR>Inv α<VAR>f g : Filter α<VAR>hf : f ≤ g<GOAL>f⁻¹ ≤ g⁻¹
<VAR>α : Type u_2<VAR>Neg α<VAR>a : α<GOAL>-pure a = pure (-a)
<VAR>α : Type u_2<VAR>Inv α<VAR>a : α<GOAL>(pure a)⁻¹ = pure a⁻¹
<VAR>α : Type u_2<VAR>Neg α<VAR>f : Filter α<GOAL>-f = ⊥ ↔ f = ⊥
<VAR>α : Type u_2<VAR>Inv α<VAR>f : Filter α<GOAL>f⁻¹ = ⊥ ↔ f = ⊥
<VAR>α : Type u_2<VAR>Inv α<VAR>f : Filter α<GOAL>f⁻¹.NeBot ↔ f.NeBot
<VAR>α : Type u_2<VAR>Neg α<VAR>f : Filter α<GOAL>(-f).NeBot ↔ f.NeBot
<VAR>α : Type u_2<VAR>Neg α<VAR>f : Filter α<GOAL>f.NeBot → (-f).NeBot
<VAR>α : Type u_2<VAR>Inv α<VAR>f : Filter α<GOAL>f.NeBot → f⁻¹.NeBot
<VAR>α : Type u_2<VAR>Neg α<VAR>f : Filter α<VAR>f.NeBot<GOAL>(-f).NeBot
<VAR>α : Type u_2<VAR>Inv α<VAR>f : Filter α<VAR>f.NeBot<GOAL>f⁻¹.NeBot
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>f : Filter α<GOAL>Filter.comap Neg.neg f = -f
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>f : Filter α<GOAL>Filter.comap Inv.inv f = f⁻¹
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>f : Filter α<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>-s ∈ -f
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>f : Filter α<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>s⁻¹ ∈ f⁻¹
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>f g : Filter α<GOAL>f⁻¹ ≤ g⁻¹ ↔ f ≤ g
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>f g : Filter α<GOAL>-f ≤ -g ↔ f ≤ g
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>f g : Filter α<GOAL>-f ≤ g ↔ f ≤ -g
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>f g : Filter α<GOAL>f⁻¹ ≤ g ↔ f ≤ g⁻¹
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>f : Filter α<GOAL>-f ≤ f ↔ -f = f
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>f : Filter α<GOAL>f⁻¹ ≤ f ↔ f⁻¹ = f
<VAR>G : Type u_7<VAR>OrderedAddCommGroup G<GOAL>-Filter.atTop = Filter.atBot
<VAR>G : Type u_7<VAR>OrderedCommGroup G<GOAL>Filter.atTop⁻¹ = Filter.atBot
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<GOAL>Filter.map₂ (fun x x_1 => x * x_1) f g = f * g
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<GOAL>Filter.map₂ (fun x x_1 => x + x_1) f g = f + g
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<VAR>s : Set α<GOAL>s ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<VAR>s : Set α<GOAL>s ∈ f + g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ + t₂ ⊆ s
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<VAR>s t : Set α<GOAL>s ∈ f → t ∈ g → s + t ∈ f + g
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<VAR>s t : Set α<GOAL>s ∈ f → t ∈ g → s * t ∈ f * g
<VAR>α : Type u_2<VAR>Add α<VAR>g : Filter α<GOAL>⊥ + g = ⊥
<VAR>α : Type u_2<VAR>Mul α<VAR>g : Filter α<GOAL>⊥ * g = ⊥
<VAR>α : Type u_2<VAR>Add α<VAR>f : Filter α<GOAL>f + ⊥ = ⊥
<VAR>α : Type u_2<VAR>Mul α<VAR>f : Filter α<GOAL>f * ⊥ = ⊥
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<GOAL>f * g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<GOAL>f + g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<GOAL>(f + g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<GOAL>(f * g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<GOAL>f.NeBot → g.NeBot → (f * g).NeBot
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<GOAL>f.NeBot → g.NeBot → (f + g).NeBot
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<GOAL>(f + g).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<GOAL>(f * g).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<GOAL>(f + g).NeBot → g.NeBot
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<GOAL>(f * g).NeBot → g.NeBot
<VAR>α : Type u_2<VAR>Mul α<VAR>f g : Filter α<VAR>f.NeBot<VAR>g.NeBot<GOAL>(f * g).NeBot
<VAR>α : Type u_2<VAR>Add α<VAR>f g : Filter α<VAR>f.NeBot<VAR>g.NeBot<GOAL>(f + g).NeBot
<VAR>α : Type u_2<VAR>Mul α<VAR>g : Filter α<VAR>a : α<GOAL>pure a * g = Filter.map (fun x => a * x) g
<VAR>α : Type u_2<VAR>Add α<VAR>g : Filter α<VAR>a : α<GOAL>pure a + g = Filter.map (fun x => a + x) g
<VAR>α : Type u_2<VAR>Mul α<VAR>f : Filter α<VAR>b : α<GOAL>f * pure b = Filter.map (fun x => x * b) f
<VAR>α : Type u_2<VAR>Add α<VAR>f : Filter α<VAR>b : α<GOAL>f + pure b = Filter.map (fun x => x + b) f
<VAR>α : Type u_2<VAR>Add α<VAR>a b : α<GOAL>pure a + pure b = pure (a + b)
<VAR>α : Type u_2<VAR>Mul α<VAR>a b : α<GOAL>pure a * pure b = pure (a * b)
<VAR>α : Type u_2<VAR>Add α<VAR>f g h : Filter α<GOAL>h ≤ f + g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s + t ∈ h
<VAR>α : Type u_2<VAR>Mul α<VAR>f g h : Filter α<GOAL>h ≤ f * g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s * t ∈ h
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>f₁ f₂ : Filter α<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>m : F<GOAL>Filter.map (⇑m) (f₁ + f₂) = Filter.map (⇑m) f₁ + Filter.map (⇑m) f₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>f₁ f₂ : Filter α<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>m : F<GOAL>Filter.map (⇑m) (f₁ * f₂) = Filter.map (⇑m) f₁ * Filter.map (⇑m) f₂
<VAR>α : Type u_2<VAR>Mul α<GOAL>⇑Filter.pureMulHom = pure
<VAR>α : Type u_2<VAR>Add α<GOAL>⇑Filter.pureAddHom = pure
<VAR>α : Type u_2<VAR>Mul α<VAR>a : α<GOAL>Filter.pureMulHom a = pure a
<VAR>α : Type u_2<VAR>Add α<VAR>a : α<GOAL>Filter.pureAddHom a = pure a
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<GOAL>Filter.map₂ (fun x x_1 => x - x_1) f g = f - g
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<GOAL>Filter.map₂ (fun x x_1 => x / x_1) f g = f / g
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<VAR>s : Set α<GOAL>s ∈ f / g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<VAR>s : Set α<GOAL>s ∈ f - g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ - t₂ ⊆ s
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<VAR>s t : Set α<GOAL>s ∈ f → t ∈ g → s - t ∈ f - g
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<VAR>s t : Set α<GOAL>s ∈ f → t ∈ g → s / t ∈ f / g
<VAR>α : Type u_2<VAR>Sub α<VAR>g : Filter α<GOAL>⊥ - g = ⊥
<VAR>α : Type u_2<VAR>Div α<VAR>g : Filter α<GOAL>⊥ / g = ⊥
<VAR>α : Type u_2<VAR>Div α<VAR>f : Filter α<GOAL>f / ⊥ = ⊥
<VAR>α : Type u_2<VAR>Sub α<VAR>f : Filter α<GOAL>f - ⊥ = ⊥
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<GOAL>f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<GOAL>f - g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<GOAL>(f - g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<GOAL>(f / g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<GOAL>f.NeBot → g.NeBot → (f / g).NeBot
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<GOAL>f.NeBot → g.NeBot → (f - g).NeBot
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<GOAL>(f - g).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<GOAL>(f / g).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<GOAL>(f - g).NeBot → g.NeBot
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<GOAL>(f / g).NeBot → g.NeBot
<VAR>α : Type u_2<VAR>Div α<VAR>f g : Filter α<VAR>f.NeBot<VAR>g.NeBot<GOAL>(f / g).NeBot
<VAR>α : Type u_2<VAR>Sub α<VAR>f g : Filter α<VAR>f.NeBot<VAR>g.NeBot<GOAL>(f - g).NeBot
<VAR>α : Type u_2<VAR>Sub α<VAR>g : Filter α<VAR>a : α<GOAL>pure a - g = Filter.map (fun x => a - x) g
<VAR>α : Type u_2<VAR>Div α<VAR>g : Filter α<VAR>a : α<GOAL>pure a / g = Filter.map (fun x => a / x) g
<VAR>α : Type u_2<VAR>Sub α<VAR>f : Filter α<VAR>b : α<GOAL>f - pure b = Filter.map (fun x => x - b) f
<VAR>α : Type u_2<VAR>Div α<VAR>f : Filter α<VAR>b : α<GOAL>f / pure b = Filter.map (fun x => x / b) f
<VAR>α : Type u_2<VAR>Sub α<VAR>a b : α<GOAL>pure a - pure b = pure (a - b)
<VAR>α : Type u_2<VAR>Div α<VAR>a b : α<GOAL>pure a / pure b = pure (a / b)
<VAR>α : Type u_2<VAR>Div α<VAR>f₁ f₂ g₁ g₂ : Filter α<GOAL>f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ / g₁ ≤ f₂ / g₂
<VAR>α : Type u_2<VAR>Sub α<VAR>f₁ f₂ g₁ g₂ : Filter α<GOAL>f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ - g₁ ≤ f₂ - g₂
<VAR>α : Type u_2<VAR>Sub α<VAR>f g₁ g₂ : Filter α<GOAL>g₁ ≤ g₂ → f - g₁ ≤ f - g₂
<VAR>α : Type u_2<VAR>Div α<VAR>f g₁ g₂ : Filter α<GOAL>g₁ ≤ g₂ → f / g₁ ≤ f / g₂
<VAR>α : Type u_2<VAR>Div α<VAR>f₁ f₂ g : Filter α<GOAL>f₁ ≤ f₂ → f₁ / g ≤ f₂ / g
<VAR>α : Type u_2<VAR>Sub α<VAR>f₁ f₂ g : Filter α<GOAL>f₁ ≤ f₂ → f₁ - g ≤ f₂ - g
<VAR>α : Type u_2<VAR>Sub α<VAR>f g h : Filter α<GOAL>h ≤ f - g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s - t ∈ h
<VAR>α : Type u_2<VAR>Div α<VAR>f g h : Filter α<GOAL>h ≤ f / g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s / t ∈ h
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulOneClass α<VAR>MulOneClass β<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>m : F<VAR>f g : Filter β<GOAL>Filter.comap (⇑m) f * Filter.comap (⇑m) g ≤ Filter.comap (⇑m) (f * g)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>m : F<VAR>f g : Filter β<GOAL>Filter.comap (⇑m) f + Filter.comap (⇑m) g ≤ Filter.comap (⇑m) (f + g)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulOneClass α<VAR>MulOneClass β<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>m : F<VAR>f₁ g₁ : Filter α<VAR>f₂ g₂ : Filter β<GOAL>Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) g₁ g₂ → Filter.Tendsto (⇑m) (f₁ * g₁) (f₂ * g₂)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>m : F<VAR>f₁ g₁ : Filter α<VAR>f₂ g₂ : Filter β<GOAL>Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) g₁ g₂ → Filter.Tendsto (⇑m) (f₁ + g₁) (f₂ + g₂)
<VAR>α : Type u_2<VAR>MulOneClass α<GOAL>⇑Filter.pureMonoidHom = pure
<VAR>α : Type u_2<VAR>AddZeroClass α<GOAL>⇑Filter.pureAddMonoidHom = pure
<VAR>α : Type u_2<VAR>MulOneClass α<VAR>a : α<GOAL>Filter.pureMonoidHom a = pure a
<VAR>α : Type u_2<VAR>AddZeroClass α<VAR>a : α<GOAL>Filter.pureAddMonoidHom a = pure a
<VAR>α : Type u_2<VAR>Monoid α<VAR>f : Filter α<VAR>s : Set α<VAR>hs : s ∈ f<VAR>n : ℕ<GOAL>s ^ n ∈ f ^ n
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>f : Filter α<VAR>s : Set α<VAR>hs : s ∈ f<VAR>n : ℕ<GOAL>n • s ∈ n • f
<VAR>α : Type u_2<VAR>Monoid α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>⊥ ^ n = ⊥
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • ⊥ = ⊥
<VAR>α : Type u_2<VAR>Monoid α<VAR>f : Filter α<VAR>hf : 1 ≤ f<GOAL>f * ⊤ = ⊤
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>f : Filter α<VAR>hf : 0 ≤ f<GOAL>f + ⊤ = ⊤
<VAR>α : Type u_2<VAR>Monoid α<VAR>f : Filter α<VAR>hf : 1 ≤ f<GOAL>⊤ * f = ⊤
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>f : Filter α<VAR>hf : 0 ≤ f<GOAL>⊤ + f = ⊤
<VAR>α : Type u_2<VAR>AddMonoid α<GOAL>⊤ + ⊤ = ⊤
<VAR>α : Type u_2<VAR>Monoid α<GOAL>⊤ * ⊤ = ⊤
<VAR>α : Type u_2<VAR>Monoid α<VAR>n : ℕ<GOAL>n ≠ 0 → ⊤ ^ n = ⊤
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>n : ℕ<GOAL>n ≠ 0 → n • ⊤ = ⊤
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>a : α<GOAL>IsAddUnit a → IsAddUnit (pure a)
<VAR>α : Type u_2<VAR>Monoid α<VAR>a : α<GOAL>IsUnit a → IsUnit (pure a)
<VAR>α : Type u_2<VAR>DivisionMonoid α<VAR>f g : Filter α<GOAL>f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
<VAR>α : Type u_2<VAR>SubtractionMonoid α<VAR>f g : Filter α<GOAL>f + g = 0 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a + b = 0
<VAR>α : Type u_2<VAR>DivisionMonoid α<VAR>f : Filter α<GOAL>IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a
<VAR>α : Type u_2<VAR>SubtractionMonoid α<VAR>f : Filter α<GOAL>IsAddUnit f ↔ ∃ a, f = pure a ∧ IsAddUnit a
<VAR>α : Type u_2<VAR>Distrib α<VAR>f g h : Filter α<GOAL>f * (g + h) ≤ f * g + f * h
<VAR>α : Type u_2<VAR>Distrib α<VAR>f g h : Filter α<GOAL>(f + g) * h ≤ f * h + g * h
<VAR>α : Type u_2<VAR>MulZeroClass α<VAR>f : Filter α<VAR>hf : f.NeBot<GOAL>0 ≤ f * 0
<VAR>α : Type u_2<VAR>MulZeroClass α<VAR>g : Filter α<VAR>hg : g.NeBot<GOAL>0 ≤ 0 * g
<VAR>α : Type u_2<VAR>AddGroup α<VAR>f g : Filter α<GOAL>0 ≤ f - g ↔ ¬Disjoint f g
<VAR>α : Type u_2<VAR>Group α<VAR>f g : Filter α<GOAL>1 ≤ f / g ↔ ¬Disjoint f g
<VAR>α : Type u_2<VAR>Group α<VAR>f g : Filter α<GOAL>¬1 ≤ f / g ↔ Disjoint f g
<VAR>α : Type u_2<VAR>AddGroup α<VAR>f g : Filter α<GOAL>¬0 ≤ f - g ↔ Disjoint f g
<VAR>α : Type u_2<VAR>AddGroup α<VAR>f : Filter α<VAR>h : f.NeBot<GOAL>0 ≤ f - f
<VAR>α : Type u_2<VAR>Group α<VAR>f : Filter α<VAR>h : f.NeBot<GOAL>1 ≤ f / f
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a : α<GOAL>IsAddUnit (pure a)
<VAR>α : Type u_2<VAR>Group α<VAR>a : α<GOAL>IsUnit (pure a)
<VAR>α : Type u_2<VAR>Group α<VAR>f : Filter α<GOAL>IsUnit f ↔ ∃ a, f = pure a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : F<VAR>f : Filter α<GOAL>Filter.map (⇑m) (-f) = -Filter.map (⇑m) f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : F<VAR>f : Filter α<GOAL>Filter.map (⇑m) f⁻¹ = (Filter.map (⇑m) f)⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : F<VAR>f₁ : Filter α<VAR>f₂ : Filter β<GOAL>Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) (-f₁) (-f₂)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : F<VAR>f₁ : Filter α<VAR>f₂ : Filter β<GOAL>Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) f₁⁻¹ f₂⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : F<VAR>f g : Filter α<GOAL>Filter.map (⇑m) (f - g) = Filter.map (⇑m) f - Filter.map (⇑m) g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : F<VAR>f g : Filter α<GOAL>Filter.map (⇑m) (f / g) = Filter.map (⇑m) f / Filter.map (⇑m) g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : F<VAR>f₁ g₁ : Filter α<VAR>f₂ g₂ : Filter β<VAR>hf : Filter.Tendsto (⇑m) f₁ f₂<VAR>hg : Filter.Tendsto (⇑m) g₁ g₂<GOAL>Filter.Tendsto (⇑m) (f₁ / g₁) (f₂ / g₂)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : F<VAR>f₁ g₁ : Filter α<VAR>f₂ g₂ : Filter β<VAR>hf : Filter.Tendsto (⇑m) f₁ f₂<VAR>hg : Filter.Tendsto (⇑m) g₁ g₂<GOAL>Filter.Tendsto (⇑m) (f₁ - g₁) (f₂ - g₂)
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>f : Filter α<VAR>hf : f.NeBot<GOAL>0 ≤ f / 0
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>g : Filter α<VAR>hg : g.NeBot<GOAL>0 ≤ 0 / g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map₂ (fun x x_1 => x • x_1) f g = f • g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map₂ (fun x x_1 => x +ᵥ x_1) f g = f +ᵥ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<VAR>t : Set β<GOAL>t ∈ f • g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<VAR>t : Set β<GOAL>t ∈ f +ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ +ᵥ t₂ ⊆ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set α<VAR>t : Set β<GOAL>s ∈ f → t ∈ g → s +ᵥ t ∈ f +ᵥ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set α<VAR>t : Set β<GOAL>s ∈ f → t ∈ g → s • t ∈ f • g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>g : Filter β<GOAL>⊥ +ᵥ g = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>g : Filter β<GOAL>⊥ • g = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<GOAL>f +ᵥ ⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<GOAL>f • ⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f +ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f • g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f +ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f.NeBot → g.NeBot → (f +ᵥ g).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f.NeBot → g.NeBot → (f • g).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f • g).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f +ᵥ g).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f • g).NeBot → g.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>(f +ᵥ g).NeBot → g.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g : Filter β<VAR>f.NeBot<VAR>g.NeBot<GOAL>(f +ᵥ g).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g : Filter β<VAR>f.NeBot<VAR>g.NeBot<GOAL>(f • g).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>g : Filter β<VAR>a : α<GOAL>pure a +ᵥ g = Filter.map (fun x => a +ᵥ x) g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>g : Filter β<VAR>a : α<GOAL>pure a • g = Filter.map (fun x => a • x) g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>b : β<GOAL>f +ᵥ pure b = Filter.map (fun x => x +ᵥ b) f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>b : β<GOAL>f • pure b = Filter.map (fun x => x • b) f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>a : α<VAR>b : β<GOAL>pure a +ᵥ pure b = pure (a +ᵥ b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>a : α<VAR>b : β<GOAL>pure a • pure b = pure (a • b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<GOAL>f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ +ᵥ g₁ ≤ f₂ +ᵥ g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<GOAL>f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ • g₁ ≤ f₂ • g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<GOAL>g₁ ≤ g₂ → f • g₁ ≤ f • g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<GOAL>g₁ ≤ g₂ → f +ᵥ g₁ ≤ f +ᵥ g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f₁ f₂ : Filter α<VAR>g : Filter β<GOAL>f₁ ≤ f₂ → f₁ • g ≤ f₂ • g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f₁ f₂ : Filter α<VAR>g : Filter β<GOAL>f₁ ≤ f₂ → f₁ +ᵥ g ≤ f₂ +ᵥ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter α<VAR>g h : Filter β<GOAL>h ≤ f +ᵥ g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s +ᵥ t ∈ h
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter α<VAR>g h : Filter β<GOAL>h ≤ f • g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s • t ∈ h
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<GOAL>Filter.map₂ (fun x x_1 => x -ᵥ x_1) f g = f -ᵥ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<VAR>s : Set α<GOAL>s ∈ f -ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<VAR>s t : Set β<GOAL>s ∈ f → t ∈ g → s -ᵥ t ∈ f -ᵥ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>g : Filter β<GOAL>⊥ -ᵥ g = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f : Filter β<GOAL>f -ᵥ ⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<GOAL>f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<GOAL>(f -ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<GOAL>f.NeBot → g.NeBot → (f -ᵥ g).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<GOAL>(f -ᵥ g).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<GOAL>(f -ᵥ g).NeBot → g.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<VAR>f.NeBot<VAR>g.NeBot<GOAL>(f -ᵥ g).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>g : Filter β<VAR>a : β<GOAL>pure a -ᵥ g = Filter.map (fun x => a -ᵥ x) g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f : Filter β<VAR>b : β<GOAL>f -ᵥ pure b = Filter.map (fun x => x -ᵥ b) f