filter_image — Mathlib

English

Filtering after image equals image after filtering by preimage condition: image f s filtered by p equals image f of s filtered by p ∘ f.

Русский

Фильтрация после образа равна образу после фильтрации по предобразному условию: image f s фильтруется равносильно image f (s фильтр по p ∘ f).

LaTeX

$$$\mathrm{filter}\ p\ (\mathrm{image}\ f\ s) = \mathrm{image}\ f\ (\mathrm{filter}\ (\lambda a. p(f\ a))\ s)$$$

Lean4

theorem filter_image {p : β → Prop} [DecidablePred p] : (s.image f).filter p = (s.filter fun a ↦ p (f a)).image f := by
  grind

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