diag_of_prod_left — Mathlib

English

If p holds eventually on (f × f) × g, then p holds eventually on f × g after flattening, with left diagonal.

Русский

Если p выполняется Eventually на (f × f) × g, тогда p выполняется Eventually на f × g после диагонализации слева.

LaTeX

$$$$\forall^\infty x \in (f \times f) \times g,\; p x \Rightarrow \forall^\infty x \in f \times g,\; p((x_1,x_1),x_2).$$$$

Lean4

theorem diag_of_prod_left {f : Filter α} {g : Filter γ} {p : (α × α) × γ → Prop} :
    (∀ᶠ x in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ x : α × γ in f ×ˢ g, p ((x.1, x.1), x.2) :=
  by
  intro h
  obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
  exact (ht.diag_of_prod.prod_mk hs).mono fun x hx => by simp only [hst hx.1 hx.2]

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