Theorems · Theorem · general topology

Filter.Eventually.diag_of_prod

∀ {α : Type u_1} {f : Filter α} {p : α × α → Prop}, (∀ᶠ (i : α × α) in f ×ˢ f, p i) → ∀ᶠ (i : α) in f, p (i, i)

A fact that is eventually true about all pairs l ×ˢ l is eventually true about all diagonal pairs (i, i)

Defined in

Mathlib.Order.Filter.Prod

Cited by

11 results in Mathlib

Foundations

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