of_subtype

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.of_subtype

English

If the subtype s is nonempty, then s is nonempty as a subset of α.

Русский

Если подтип s непуст, то s как множество также непусто.

LaTeX

$$$$ \forall {\,s : \mathrm{Set}\,\alpha}, \operatorname{Nonempty}(s.Elem) \Rightarrow \operatorname{Nonempty}(s). $$$$

Lean4

theorem of_subtype [Nonempty (↥s)] : s.Nonempty :=
  nonempty_subtype.mp ‹_›

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

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

Разделы

Аффилиация

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