mem_univ

Mathlib.Data.Set.Operations

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

English

For every x, x is an element of the universal set univ.

Русский

Для каждого x выполняется, что x лежит в универсальном множестве univ.

LaTeX

$$$x \\in \\mathrm{univ}$$$

Lean4

@[simp, mfld_simps, grind]
theorem mem_univ (x : α) : x ∈ @univ α :=
  trivial

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

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

Разделы

Аффилиация

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