Filter.Germ.coe_lt

theorem Filter.Germ.coe_lt : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : Preorder β] {f g : α → β}, ↑f < ↑g ↔ ∀ᶠ (x : α) in ↑φ, f x < g x

This theorem, `Filter.Germ.coe_lt`, states that for any types `α` and `β`, any ultrafilter `φ` on `α`, any preorder structure on `β`, and any functions `f` and `g` from `α` to `β`, the lifting of `f` to the germ of `φ` is less than the lifting of `g` to the germ of `φ` if and only if for almost all `x` in `α` with respect to `φ`, `f(x)` is less than `g(x)`. In other words, it's about the order relationship between the filter germs of `f` and `g` under certain conditions.

More concisely: Given types `α`, `β`, an ultrafilter `φ` on `α`, a preorder `≤` on `β`, and functions `f` and `g` from `α` to `β`, the germ of `f` is less than the germ of `g` with respect to `φ` if and only if `f(x) ≤ g(x)` holds for almost all `x` in `α` with respect to `φ`.