diag_of_prod — Mathlib

English

If p is a predicate on α×α and p holds eventually on f × f, then p holds eventually on the diagonal i ↦ (i,i).

Русский

Если для предиката p на α×α верно, что p выполняется Eventually на f×f, то p выполняется Eventually на диагонали i ↦ (i,i).

LaTeX

$$$$\big( \forall^\infty i \in f \times f,\; p(i) \big) \Rightarrow \forall^\infty i \in f,\; p(i,i).$$$$

Lean4

/-- A fact that is eventually true about all pairs `l ×ˢ l` is eventually true about
all diagonal pairs `(i, i)` -/
theorem diag_of_prod {p : α × α → Prop} (h : ∀ᶠ i in f ×ˢ f, p i) : ∀ᶠ i in f, p (i, i) :=
  h.image_of_prod (r := p.curry) tendsto_id

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