pure_seq_eq_map — Mathlib

English

For any g and f, seq (pure g) f = map g f.

Русский

Для любых g и f, seq (pure g) f = map g f.

LaTeX

$$$ \text{seq } (\mathrm{pure} \, g) \, f = \mathrm{map} \, g \, f $$$

Lean4

@[simp]
theorem pure_seq_eq_map (g : α → β) (f : Filter α) : seq (pure g) f = f.map g :=
  by
  refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)
  · rw [← singleton_seq]
    apply seq_mem_seq _ hs
    exact singleton_mem_pure
  · refine sets_of_superset (map g f) (image_mem_map ht) ?_
    rintro b ⟨a, ha, rfl⟩
    exact ⟨g, hs, a, ha, rfl⟩

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