nonempty_of_nonempty_type

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.nonempty_of_nonempty_type

English

If x has a nonempty type, then x is nonempty as a PSet.

Русский

Если у x есть непустый тип, то x является непустым как PSet.

LaTeX

$$$\\forall x:\\mathrm{PSet}, [\\mathrm{Nonempty} x.Type] \\rightarrow x\\Nonempty$$$

Lean4

theorem nonempty_of_nonempty_type (x : PSet) [h : Nonempty x.Type] : PSet.Nonempty x :=
  nonempty_type_iff_nonempty.1 h

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

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

Разделы

Аффилиация

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