range_nonempty_iff_nonempty

Mathlib.Data.Set.Image

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

English

(range f).Nonempty ↔ Nonempty ι.

Русский

Не пустой диапазон образа эквивалентен не пустому индексу.

LaTeX

$$$ (\\operatorname{range} f).\\operatorname{Nonempty} \\;\\iff\\; \\operatorname{Nonempty} \\ ι $$$

Lean4

theorem range_nonempty_iff_nonempty : (range f).Nonempty ↔ Nonempty ι :=
  ⟨fun ⟨_, x, _⟩ => ⟨x⟩, fun ⟨x⟩ => ⟨f x, mem_range_self x⟩⟩

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

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

Разделы

Аффилиация

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