exists_of_mem_map

Mathlib.Data.Stream.Init

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

Lean4

theorem exists_of_mem_map {f} {b : β} {s : Stream' α} : b ∈ map f s → ∃ a, a ∈ s ∧ f a = b := fun ⟨n, h⟩ =>
  ⟨get s n, ⟨n, rfl⟩, h.symm⟩

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

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

Разделы

Аффилиация

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