filter_product — Mathlib

English

Let p : α → Prop and q : β → Prop. Then ((s × t).filter (x ↦ p x.1 ∧ q x.2)) = (s.filter p) × (t.filter q).

Русский

Пусть p : α → Prop и q : β → Prop. Тогда ((s × t).filter (λ x, p x.1 ∧ q x.2)) равно (s.filter p) × (t.filter q).

LaTeX

$$$((s \\\\times t).filter (\\\\lambda x: (p x.1) \\\\land (q x.2))) = (s.\\\\text{filter} p) \\\\times (t.\\\\text{filter} q)$$$

Lean4

theorem filter_product (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] :
    ((s ×ˢ t).filter fun x : α × β => p x.1 ∧ q x.2) = s.filter p ×ˢ t.filter q := by grind

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