Theorems · Theorem · general topology

Filter.EventuallyEq.trans_le

∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g h : α → β}, f =ᶠ[l] g → g ≤ᶠ[l] h → f ≤ᶠ[l] h

Defined in

Mathlib.Order.Filter.Basic

Cited by

4 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

Preorder