exists_mem_map

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.exists_mem_map

English

There exists y in o.map f with p y iff there exists x in o with p (f x).

Русский

Существует y в o.map f такое, что p(y), тогда и только тогда существует x ∈ o с p(f(x)).

LaTeX

$$$$ (\exists y \in o.map f, p y) \iff \exists x \in o, p (f x). $$$$

Lean4

theorem exists_mem_map {f : α → β} {o : Option α} {p : β → Prop} : (∃ y ∈ o.map f, p y) ↔ ∃ x ∈ o, p (f x) := by simp

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

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

Разделы

Аффилиация

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