filterMap — Mathlib

English

Given a suitable option-valued function f, nodup of s implies nodup of filterMap f s.

Русский

При заданной подходящей функции f, если s без повторов, то filterMap f s также без повторов.

LaTeX

$$$ (\\forall a,a',b, b \\in f a \\,\\to\\, b \\in f a' \\to a = a') \\to s.Nodup \\to (\\mathrm{filterMap} f\\ s).Nodup $$$

Lean4

protected theorem filterMap (f : α → Option β) (H : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
    Nodup s → Nodup (filterMap f s) :=
  Quot.induction_on s fun _ => List.Nodup.filterMap H

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