mapsTo_univ

Mathlib.Data.Set.Function

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

English

MapsTo f s univ holds for any f and s.

Русский

Для любых f и s отображение f на s в множество world-univ существует.

LaTeX

$$$\\\\MapsTo f s \\mathrm{Set.univ}$$$

Lean4

theorem mapsTo_univ (f : α → β) (s : Set α) : MapsTo f s univ := fun _ _ => trivial

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

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

Разделы

Аффилиация

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