Documentation

Mathlib.Order.Filter.Ring

Lemmas about filters and ordered rings. #

theorem Filter.EventuallyLE.mul_le_mul {α : Type u} {β : Type v} [MulZeroClass β] [PartialOrder β] [PosMulMono β] [MulPosMono β] {l : Filter α} {f₁ : αβ} {f₂ : αβ} {g₁ : αβ} {g₂ : αβ} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁) (hf₀ : 0 ≤ᶠ[l] f₂) :
f₁ * g₁ ≤ᶠ[l] f₂ * g₂
theorem Filter.EventuallyLE.add_le_add {α : Type u} {β : Type v} [Add β] [Preorder β] [CovariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 x2] [CovariantClass β β (Function.swap fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 x2] {l : Filter α} {f₁ : αβ} {f₂ : αβ} {g₁ : αβ} {g₂ : αβ} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ + g₁ ≤ᶠ[l] f₂ + g₂
theorem Filter.EventuallyLE.mul_le_mul' {α : Type u} {β : Type v} [Mul β] [Preorder β] [CovariantClass β β (fun (x1 x2 : β) => x1 * x2) fun (x1 x2 : β) => x1 x2] [CovariantClass β β (Function.swap fun (x1 x2 : β) => x1 * x2) fun (x1 x2 : β) => x1 x2] {l : Filter α} {f₁ : αβ} {f₂ : αβ} {g₁ : αβ} {g₂ : αβ} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ * g₁ ≤ᶠ[l] f₂ * g₂
theorem Filter.EventuallyLE.mul_nonneg {α : Type u} {β : Type v} [OrderedSemiring β] {l : Filter α} {f : αβ} {g : αβ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) :
0 ≤ᶠ[l] f * g
theorem Filter.eventually_sub_nonneg {α : Type u} {β : Type v} [OrderedRing β] {l : Filter α} {f : αβ} {g : αβ} :
0 ≤ᶠ[l] g - f f ≤ᶠ[l] g
instance Filter.Germ.instOrderedAddCommGroup {α : Type u} {β : Type v} {l : Filter α} [OrderedAddCommGroup β] :
Equations
theorem Filter.Germ.instOrderedAddCommGroup.proof_2 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (a : l.Germ β) :
theorem Filter.Germ.instOrderedAddCommGroup.proof_1 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (a : l.Germ β) (b : l.Germ β) :
a - b = a + -b
theorem Filter.Germ.instOrderedAddCommGroup.proof_4 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (n : ) (a : l.Germ β) :
theorem Filter.Germ.instOrderedAddCommGroup.proof_6 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (a : l.Germ β) (b : l.Germ β) :
a + b = b + a
theorem Filter.Germ.instOrderedAddCommGroup.proof_3 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (n : ) (a : l.Germ β) :
theorem Filter.Germ.instOrderedAddCommGroup.proof_5 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (a : l.Germ β) :
-a + a = 0
theorem Filter.Germ.instOrderedAddCommGroup.proof_7 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (a : l.Germ β) (b : l.Germ β) :
a b∀ (c : l.Germ β), c + a c + b
instance Filter.Germ.instOrderedCommGroup {α : Type u} {β : Type v} {l : Filter α} [OrderedCommGroup β] :
OrderedCommGroup (l.Germ β)
Equations
instance Filter.Germ.instOrderedSemiring {α : Type u} {β : Type v} {l : Filter α} [OrderedSemiring β] :
OrderedSemiring (l.Germ β)
Equations
instance Filter.Germ.instOrderedCommSemiring {α : Type u} {β : Type v} {l : Filter α} [OrderedCommSemiring β] :
Equations
instance Filter.Germ.instOrderedRing {α : Type u} {β : Type v} {l : Filter α} [OrderedRing β] :
OrderedRing (l.Germ β)
Equations
instance Filter.Germ.instOrderedCommRing {α : Type u} {β : Type v} {l : Filter α} [OrderedCommRing β] :
OrderedCommRing (l.Germ β)
Equations