monotone_filter_right — Mathlib

English

If p implies q pointwise, then filter p s ≤ filter q s for any s.

Русский

Если p слево по каждому элементу имплицирует q, то filter p s ≤ filter q s для любого s.

LaTeX

$$$\\left(\\forall b, p(b) \\Rightarrow q(b)\right) \\Rightarrow \\mathrm{filter}_p(s) \\le \\mathrm{filter}_q(s)$$

Lean4

theorem monotone_filter_right (s : Multiset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q]
    (h : ∀ b, p b → q b) : s.filter p ≤ s.filter q :=
  Quotient.inductionOn s fun l => (l.monotone_filter_right <| by simpa using h).subperm

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