eventuallyEq_bind — Mathlib

English

For functions g1,g2: β → γ, we have g1 =ᶠ[bind f m] g2 iff ∀ᶠ x in f, g1 =ᶠ[m x] g2.

Русский

Для функций g1,g2: β → γ верно g1 =ᶠ[bind f m] g2 тогда и только тогда, когда ∀ᶠ x в f, g1 =ᶠ[m x] g2.

LaTeX

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

Lean4

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

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