forall_mem_image

Mathlib.Data.Finset.Image

URI: https://scilib.ai/kg/mathlib#Finset.forall_mem_image

English

For all p, (for all y in image f s, p(y)) holds iff (for all x in s, p(f(x))).

Русский

Для всех p: (для всех y ∈ image f s верно p(y)) эквивалентно (для всех x ∈ s верно p(f(x))).

LaTeX

$$$\\Big( \\forall y \\in \\operatorname{image}(f,s), p(y) \\Big) \\iff \\forall x \\in s, p(f(x))$$$

Lean4

theorem forall_mem_image {p : β → Prop} : (∀ y ∈ s.image f, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x) := by simp

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

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

Разделы

Аффилиация

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