mem_filterMap — Mathlib

English

An element b belongs to filterMap f s precisely when there exists a in s such that f a = some b.

Русский

Элемент b принадлежит filterMap f s тогда и только тогда, когда существует a ∈ s с f a = some b.

LaTeX

$$$b \in \operatorname{filterMap} f s \iff \exists a, a \in s \land f a = \text{some } b$$$

Lean4

@[simp]
theorem mem_filterMap (f : α → Option β) (s : Multiset α) {b : β} : b ∈ filterMap f s ↔ ∃ a, a ∈ s ∧ f a = some b :=
  Quot.inductionOn s fun _ => List.mem_filterMap

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