prod_inl — Mathlib

English

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

Русский

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

LaTeX

$$$$\forall^{\infty} x \in la \timesˢ lb, p (x.1).$$$$

Lean4

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

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