exists_mem_image

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.exists_mem_image

English

(∃ y ∈ f '' s, p y) ↔ (∃ x ∈ s, p (f x)).

Русский

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

LaTeX

$$$ (\\exists y \\in f''s, p(y)) \\iff (\\exists x \\in s, p(f(x))). $$$

Lean4

theorem exists_mem_image {f : α → β} {s : Set α} {p : β → Prop} : (∃ y ∈ f '' s, p y) ↔ ∃ x ∈ s, p (f x) := by simp

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

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

Разделы

Аффилиация

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