mem_image_of_mem

Mathlib.Data.Finset.Image

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

English

If a ∈ s then f(a) ∈ image f s.

Русский

Если a ∈ s, то f(a) ∈ image f s.

LaTeX

$$$a \\in s \\Rightarrow f(a) \\in \\operatorname{image}(f,s)$$$

Lean4

theorem mem_image_of_mem (f : α → β) {a} (h : a ∈ s) : f a ∈ s.image f :=
  mem_image.2 ⟨_, h, rfl⟩

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

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

Разделы

Аффилиация

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