eventually_and — Mathlib

English

The property that p x and q x holds eventually is equivalent to p x holds eventually and q x holds eventually.

Русский

Свойство, что p x и q x выполняются часто, эквивалентно тому, что p x выполняется часто и q x выполняется часто.

LaTeX

$$$ (\forall^\infty x \in f,\ p x \land q x) \leftrightarrow (\forall^\infty x \in f,\ p x) \land (\forall^\infty x \in f,\ q x) $$$

Lean4

@[simp]
theorem eventually_and {p q : α → Prop} {f : Filter α} : (∀ᶠ x in f, p x ∧ q x) ↔ (∀ᶠ x in f, p x) ∧ ∀ᶠ x in f, q x :=
  inter_mem_iff

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