mem_filter — Mathlib

English

For π a prepartition and p a predicate on boxes, J belongs to π.filter p iff J ∈ π and p J.

Русский

Для предразбиения π и предиката p на коробки, элемент J принадлежит π.filter p тогда и только тогда, когда J ∈ π и p J.

LaTeX

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

Lean4

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

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