seq_pure — Mathlib

English

The same as above: seq (pure g) f = map g f.

Русский

То же самое: seq (pure g) f = map g f.

LaTeX

$$$ \operatorname{seq} (\operatorname{pure} g) f = \operatorname{map} g f $$$

Lean4

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

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