classToCong_empty

Mathlib.SetTheory.ZFC.Class

URI: https://scilib.ai/kg/mathlib#Class.classToCong_empty

English

The conglomerate of the empty class is the empty conglomerate.

Русский

Конгломерат пустого класса равен пустому конгломерату.

LaTeX

$$$\\operatorname{classToCong}(\\varnothing) = \\varnothing$$$

Lean4

@[simp]
theorem classToCong_empty : classToCong ∅ = ∅ := by simp [classToCong]

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

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

Разделы

Аффилиация

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