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 (x x_1 : β) => x + x_1) fun (x x_1 : β) => x ≤ x_1] [CovariantClass β β (Function.swap fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x ≤ x_1] {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 (x x_1 : β) => x * x_1) fun (x x_1 : β) => x ≤ x_1] [CovariantClass β β (Function.swap fun (x x_1 : β) => x * x_1) fun (x x_1 : β) => x ≤ x_1] {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

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

instance Filter.Germ.instOrderedAddCommGroup {α : Type u} {β : Type v} {l : Filter α} [OrderedAddCommGroup β] : OrderedAddCommGroup (l.Germ β)

Equations

• Filter.Germ.instOrderedAddCommGroup = let __spread.0 := Filter.Germ.instOrderedAddCancelCommMonoid; let __spread.1 := Filter.Germ.instAddCommGroup; OrderedAddCommGroup.mk ⋯

theorem Filter.Germ.instOrderedAddCommGroup.proof_4 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (n : ℕ) (a : l.Germ β) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a

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

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_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 β) : SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a

theorem Filter.Germ.instOrderedAddCommGroup.proof_2 {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedAddCommGroup β] (a : l.Germ β) : SubNegMonoid.zsmul 0 a = 0

instance Filter.Germ.instOrderedCommGroup {α : Type u} {β : Type v} {l : Filter α} [OrderedCommGroup β] : OrderedCommGroup (l.Germ β)

Equations

• Filter.Germ.instOrderedCommGroup = let __spread.0 := Filter.Germ.instOrderedCancelCommMonoid; let __spread.1 := Filter.Germ.instCommGroup; OrderedCommGroup.mk ⋯

instance Filter.Germ.instOrderedSemiring {α : Type u} {β : Type v} {l : Filter α} [OrderedSemiring β] : OrderedSemiring (l.Germ β)

Equations

• Filter.Germ.instOrderedSemiring = let __spread.0 := Filter.Germ.instSemiring; let __spread.1 := Filter.Germ.instOrderedAddCommMonoid; OrderedSemiring.mk ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instOrderedCommSemiring {α : Type u} {β : Type v} {l : Filter α} [OrderedCommSemiring β] : OrderedCommSemiring (l.Germ β)

Equations

• Filter.Germ.instOrderedCommSemiring = let __spread.0 := Filter.Germ.instOrderedSemiring; let __spread.1 := Filter.Germ.instCommSemiring; OrderedCommSemiring.mk ⋯

instance Filter.Germ.instOrderedRing {α : Type u} {β : Type v} {l : Filter α} [OrderedRing β] : OrderedRing (l.Germ β)

Equations

• One or more equations did not get rendered due to their size.

instance Filter.Germ.instOrderedCommRing {α : Type u} {β : Type v} {l : Filter α} [OrderedCommRing β] : OrderedCommRing (l.Germ β)

Equations

• Filter.Germ.instOrderedCommRing = let __spread.0 := Filter.Germ.instOrderedRing; let __spread.1 := Filter.Germ.instOrderedCommSemiring; OrderedCommRing.mk ⋯