filter_comm — Mathlib

English

The order of filtering by predicates p and q on a finite set does not matter.

Русский

Порядок фильтрации по предикатам p и q на конечном множестве не имеет значения.

LaTeX

$$$(s.filter p).filter q = (s.filter q).filter p$$$

Lean4

theorem filter_comm (s : Finset α) : (s.filter p).filter q = (s.filter q).filter p := by
  grind
    -- We can replace an application of filter where the decidability is inferred in "the wrong way".

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