instNonemptyElemImage

Mathlib.Data.Set.Image

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

English

If S is nonempty, then the image f[S] has a nonempty element (as a member of the image).

Русский

Если S непусто, то образ f[S] имеет непустый элемент (как элемент образа).

LaTeX

$$$$ S \text{ Nonempty } \Rightarrow (f''S).Elem \neq \varnothing. $$$$

Lean4

instance (f : α → β) (s : Set α) [Nonempty s] : Nonempty (f '' s) :=
  (Set.Nonempty.image f .of_subtype).to_subtype

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

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

Разделы

Аффилиация

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