mem_filterMap — Mathlib

English

For any b ∈ β, b ∈ s.filterMap f f_inj iff ∃ a ∈ s with f a = some b.

Русский

Для любого b ∈ β верно, что b ∈ s.filterMap f f_inj тогда и только тогда, когда существует a ∈ s такое, что f a = some b.

LaTeX

$$$ b \\in s.filterMap f f_{inj} \\iff \\exists a \\in s, f a = some b $$$

Lean4

@[simp, grind =]
theorem mem_filterMap {b : β} : b ∈ s.filterMap f f_inj ↔ ∃ a ∈ s, f a = some b :=
  s.val.mem_filterMap f

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