mk_Prop

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_Prop

English

Let Prop denote the type of truth values; it has exactly two elements, so its cardinality is 2.

Русский

Пусть Prop обозначает тип истинностных значений; он содержит ровно два элемента, поэтому его кардинал равен 2.

LaTeX

$$$|\mathrm{Prop}| = 2$$$

Lean4

theorem mk_Prop : #Prop = 2 := by simp

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

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

Разделы

Аффилиация

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