subset_range

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.BijOn.subset_range

English

If f is bijective from s onto t, then t is contained in the range of f.

Русский

Если f биекция с множества s на t, то t ⊆ Образ(f).

LaTeX

$$$\\text{BijOn}(f,s,t)\\Rightarrow t\\subseteq\\operatorname{range}(f)$$$

Lean4

theorem subset_range (h : BijOn f s t) : t ⊆ range f :=
  h.surjOn.subset_range

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

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

Разделы

Аффилиация

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