# Lemmas about filters and ordered rings. #

source
theorem Filter.EventuallyLE.mul_le_mul {α : Type u} {β : Type v} [MulZeroClass β] [Preorder β] [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₂
source
theorem Filter.EventuallyLE.mul_le_mul' {α : Type u} {β : Type v} [Mul β] [Preorder β] [MulLeftMono β] [MulRightMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ * g₁ ≤ᶠ[l] f₂ * g₂
source
theorem Filter.EventuallyLE.add_le_add {α : Type u} {β : Type v} [Add β] [Preorder β] [AddLeftMono β] [AddRightMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ + g₁ ≤ᶠ[l] f₂ + g₂
source
theorem Filter.EventuallyLE.mul_nonneg {α : Type u} {β : Type v} [Semiring β] [PartialOrder β] [IsOrderedRing β] {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) :
0 ≤ᶠ[l] f * g
source
theorem Filter.eventually_sub_nonneg {α : Type u} {β : Type v} [Ring β] [PartialOrder β] [IsOrderedRing β] {l : Filter α} {f g : α → β} :
0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g
source
instance Filter.Germ.instIsOrderedRing {α : Type u} {β : Type v} {l : Filter α} [Semiring β] [PartialOrder β] [IsOrderedRing β] :
IsOrderedRing (l.Germ β)