mem_map

Mathlib.Data.Seq.Basic

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

English

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

Русский

Если a принадлежит s, то f a принадлежит map f s.

LaTeX

$$$\forall {a} {s : Seq \alpha}, a \in s \Rightarrow f a \in map f s$$$

Lean4

theorem mem_map (f : α → β) {a : α} : ∀ {s : Seq α}, a ∈ s → f a ∈ map f s
  | ⟨_, _⟩ => Stream'.mem_map (Option.map f)

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

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

Разделы

Аффилиация

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