English
Frequent occurrence of p on the product equals the conjunction of frequent occurrences on each factor: (∃ᶠ x ∈ f × g, p x.1 ∧ q x.2) ↔ (∃ᶠ a ∈ f, p a) ∧ ∃ᶠ b ∈ g, q b.
Русский
Частое появление p на произведении равно сочетанию частого появления p на первом и q на втором факторе.
LaTeX
$$$ (\\exists^\\! x \\in f \\times\\! g, p x.1 \\wedge q x.2) \\iff (\\exists^\\! a \\in f, p a) \\wedge (\\exists^\\! b \\in g, q b) $$$
Lean4
/-- `p ∧ q` occurs frequently along the product of two filters
iff both `p` and `q` occur frequently along the corresponding filters. -/
theorem frequently_prod_and {p : α → Prop} {q : β → Prop} :
(∃ᶠ x in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ a in f, p a) ∧ ∃ᶠ b in g, q b :=
by
simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]
rfl
