filter_inter — Mathlib

English

Let p be a predicate. Then filter p (s ∩ t) = filter p s ∩ filter p t.

Русский

Пусть задано предикат p. Тогда фильтрация по пересечению равна пересечению фильтраций: filter p (s ∩ t) = filter p s ∩ filter p t.

LaTeX

$$$ \\operatorname{filter}(p, s \\cap t) = \\operatorname{filter}(p, s) \\cap \\operatorname{filter}(p, t) $$$

Lean4

@[simp]
theorem filter_inter (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s ∩ t) = filter p s ∩ filter p t :=
  le_antisymm (le_inter (filter_le_filter _ inter_le_left) (filter_le_filter _ inter_le_right)) <|
    le_filter.2 ⟨inf_le_inf (filter_le _ _) (filter_le _ _), fun _a h => of_mem_filter (mem_of_le inter_le_left h)⟩

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