preimage_range

Mathlib.Data.Set.Image

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

English

For any f, the preimage of its range is the whole domain: f^{-1}(range f) = univ.

Русский

Для любой f предобраз диапазона f равен всему объединению области определения: f^{-1}(range f) = univ.

LaTeX

$$$$ f^{-1}(\\operatorname{range}(f)) = \\operatorname{univ} $$$$

Lean4

@[simp]
theorem preimage_range (f : α → β) : f ⁻¹' range f = univ :=
  eq_univ_of_forall mem_range_self

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

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

Разделы

Аффилиация

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