eventuallyLE_iff_all_subsets — Mathlib

English

For f,g : α → β and l a filter with β a partially ordered set, f ≤ᶠ[l] g iff for every subset s of α, f and g satisfy f(x) ≤ g(x) eventually on s.

Русский

Для f,g : α → β и l — фильтр, β частично упорядованно; f ≤ᶠ[l] g тогда и только тогда, когда для каждого подмножества s ⊆ α выполняется, что f(x) ≤ g(x) адресно на s по l (в смысле eventually).

LaTeX

$$$ f ≤ᶠ[l] g \\iff ∀ s : Set α, ∀ᶠ x in l, x ∈ s \\to f x ≤ g x $$$

Lean4

theorem eventuallyLE_iff_all_subsets {f g : α → β} {l : Filter α} :
    f ≤ᶠ[l] g ↔ ∀ s : Set α, ∀ᶠ x in l, x ∈ s → f x ≤ g x :=
  eventually_iff_all_subsets

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