diag_of_prod_right — Mathlib

English

If p holds eventually on (f × g) × g, then p holds eventually on f × g with right diagonal.

Русский

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

LaTeX

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

Lean4

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

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