prod_mk — Mathlib

English

If la eventually ensures pa and lb eventually ensures pb, then the pair predicate pa and pb holds eventually on la ×ˢ lb.

Русский

Если la обеспечивает pa и lb обеспечивает pb, то pa и pb выполняются Eventually на la × lb.

LaTeX

$$$$\forall^{\infty} p \in la \times lb, \; (pa(p.1) \land pb(p.2)).$$$$

Lean4

theorem prod_mk {la : Filter α} {pa : α → Prop} (ha : ∀ᶠ x in la, pa x) {lb : Filter β} {pb : β → Prop}
    (hb : ∀ᶠ y in lb, pb y) : ∀ᶠ p in la ×ˢ lb, pa (p : α × β).1 ∧ pb p.2 :=
  (ha.prod_inl lb).and (hb.prod_inr la)

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