mem_range_of_mem_image

Mathlib.Data.Set.Image

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

English

If x ∈ f'' s then x ∈ range f.

Русский

Если x ∈ f'' s, то x ∈ range f.

LaTeX

$$$ x \\in f'' s \\Rightarrow x \\in \\operatorname{range} f $$$

Lean4

theorem mem_range_of_mem_image (f : α → β) (s) {x : β} (h : x ∈ f '' s) : x ∈ range f :=
  image_subset_range f s h

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

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

Разделы

Аффилиация

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