EventuallyLE — Mathlib

English

A function f is eventually less than or equal to a function g at a filter l if ∀ᶠ x in l, f(x) ≤ g(x).

Русский

Функция f эквивалентна или меньше, чем g вдоль фильтра l, если ∀ᶠ x ∈ l, f(x) ≤ g(x).

LaTeX

$$$\\mathrm{EventuallyLE}[\\le]\\; (l : \\mathrm{Filter}\\ \\alpha)\\ (f,g : \\alpha \\to \\beta) : \\mathrm{Prop} \\;:=\\; \\forall^{\\infty} x \\in l, f(x) \\le g(x)$$$

Lean4

/-- A function `f` is eventually less than or equal to a function `g` at a filter `l`. -/
def EventuallyLE [LE β] (l : Filter α) (f g : α → β) : Prop :=
  ∀ᶠ x in l, f x ≤ g x

Похожие утверждения