coe_filterMap — Mathlib

English

(s.filterMap f f_inj) as a Set equals { b | ∃ a ∈ s, f a = some b }.

Русский

Построение через приведение к множеству: образ filterMap равен множеству { b | ∃ a ∈ s, f a = some b }.

LaTeX

$$$ (s.filterMap f f_{inj} : Set \\beta) = { b \\mid \\exists a \\in s, f a = some b } $$$

Lean4

@[simp, norm_cast]
theorem coe_filterMap : (s.filterMap f f_inj : Set β) = {b | ∃ a ∈ s, f a = some b} :=
  Set.ext (by simp only [mem_coe, mem_filterMap, Set.mem_setOf_eq, implies_true])

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