mem_filter — Mathlib

English

For any predicate p on boxes, membership in the filtered set π.filter p is equivalent to membership in π together with the predicate p applied to the box.

Русский

Для любого предиката p над коробками, членство в отфильтрованном наборе π.filter p эквивалентно членству в π вместе с применением p к данной коробке.

LaTeX

$$$ J \\in \\pi.filter p \\iff J \\in \\pi \\land p J $$$

Lean4

@[simp]
theorem mem_filter {p : Box ι → Prop} : J ∈ π.filter p ↔ J ∈ π ∧ p J := by classical exact Finset.mem_filter

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