Lemmas about filters and ordered rings. #
theorem
Filter.EventuallyLE.mul_nonneg
{α : Type u}
{β : Type v}
[Semiring β]
[PartialOrder β]
[IsOrderedRing β]
{l : Filter α}
{f g : α → β}
(hf : 0 ≤ᶠ[l] f)
(hg : 0 ≤ᶠ[l] g)
:
theorem
Filter.eventually_sub_nonneg
{α : Type u}
{β : Type v}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{l : Filter α}
{f g : α → β}
:
instance
Filter.Germ.instIsOrderedRing
{α : Type u}
{β : Type v}
{l : Filter α}
[Semiring β]
[PartialOrder β]
[IsOrderedRing β]
:
IsOrderedRing (l.Germ β)