filter_product_left — Mathlib

English

Let p : α → Prop. Then ((s × t).filter (λ x, p x.1)) = (s.filter p) × t.

Русский

Пусть p : α → Prop. Тогда ((s × t).filter (λ x, p x.1)) = (s.filter p) × t.

LaTeX

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

Lean4

theorem filter_product_left (p : α → Prop) [DecidablePred p] :
    ((s ×ˢ t).filter fun x : α × β => p x.1) = s.filter p ×ˢ t := by simpa using filter_product p fun _ => true

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