monotone_filter_right — Mathlib

English

If p implies q pointwise, then filtering a list with p yields a sublist of filtering it with q.

Русский

Если для всех элементов p(a) ⇒ q(a), то l.filter p является подсписком l.filter q.

LaTeX

$$$\forall l:\, List\;\alpha,\; \forall p,q:\alpha\to Bool,\; (\forall a, p(a) \rightarrow q(a)) \rightarrow (l.filter p) \ <+\ l.filter q$$$

Lean4

theorem monotone_filter_right (l : List α) ⦃p q : α → Bool⦄ (h : ∀ a, p a → q a) : l.filter p <+ l.filter q := by
  induction l with grind

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