mem_map

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.mem_map

← MathLib Explorer

English

If a is in s, then f a is in map f s.

Русский

Если a ∈ s, то f a ∈ map f s.

LaTeX

$$$$ a \\in s \\;\\Rightarrow\\; f(a) \\in \\mathrm{map}(f,s) $$$$

Lean4

theorem mem_map (f : α → β) {a : α} {s : WSeq α} : a ∈ s → f a ∈ map f s :=
  Seq.mem_map
    (Option.map f)
      -- The converse is not true without additional assumptions

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru