prod_inr — Mathlib

English

If a property p holds eventually in lb, then it holds eventually for the second component in la ×ˢ lb.

Русский

Если свойство p выполняется Eventually в lb, то оно выполняется Eventually для второй компоненты в la × lb.

LaTeX

$$$$\\forall^{\\infty} y \\in lb, p(y).$$$$

Lean4

theorem prod_inr {lb : Filter β} {p : β → Prop} (h : ∀ᶠ x in lb, p x) (la : Filter α) :
    ∀ᶠ x in la ×ˢ lb, p (x : α × β).2 :=
  tendsto_snd.eventually h

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