Theorems · Theorem · general topology

Filter.Eventually.eventually_prod_of_eventually_swap

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} [g.NeBot] {p : α → β → Prop}
  {q : β → γ → Prop} {r : α → γ → Prop},
  (∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y) →
    (∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z) →
      (∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z) → ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2

A technical lemma which is a generalization of Filter.Eventually.trans_prod.

Defined in

Mathlib.Order.Filter.Prod

Cited by

1 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Filter.NeBot