Nonempty

Mathlib.SetTheory.ZFC.PSet

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

English

Equality of Set membership between toSet and original membership.

Русский

Равенство принадлежности между toSet и исходной принадлежностью.

LaTeX

$$$\\forall (a u), Eq (Set.instMembership.mem u.toSet a) (PSet.instMembership.mem u a)$$$

Lean4

/-- A nonempty set is one that contains some element. -/
protected def Nonempty (u : PSet) : Prop :=
  u.toSet.Nonempty

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

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

Разделы

Аффилиация

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