Theorems · Theorem · general topology

Filter.Eventually.diag_of_prod_right

∀ {α : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter γ} {p : α × γ × γ → Prop},
  (∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)

Defined in

Mathlib.Order.Filter.Prod

Cited by

4 results in Mathlib

Foundations

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