eventuallyLE_bind — Mathlib

English

For a partial order on γ, g1 ≤ᶠ[bind f m] g2 iff ∀ᶠ x in f, g1 ≤ᶠ[m x] g2.

Русский

Для частичного порядка на γ верно: g1 ≤ᶠ[bind f m] g2 тогда и только тогда, когда ∀ᶠ x ∈ f, g1 ≤ᶠ[m x] g2.

LaTeX

$$$g_1 \\leq^\\!_{bind\\,f\\,m} g_2 \\iff \\forall^\\infty x \\in f,\\ g_1 \\leq^\\!_{m x} g_2$$$

Lean4

@[simp]
theorem eventuallyLE_bind [LE γ] {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} :
    g₁ ≤ᶠ[bind f m] g₂ ↔ ∀ᶠ x in f, g₁ ≤ᶠ[m x] g₂ :=
  Iff.rfl

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