univ_Prop

Mathlib.Data.Fintype.Sets

URI: https://scilib.ai/kg/mathlib#Fintype.univ_Prop

English

The finite universe of propositions is exactly {True, False}.

Русский

Конечная вселенная propositions равна ровно {True, False}.

LaTeX

$$$\mathrm{Finset.univ}_{Prop} = \{ True, False \}$$$

Lean4

@[simp]
theorem univ_Prop : (Finset.univ : Finset Prop) = { True, False } :=
  Finset.eq_of_veq <| by simp; rfl

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

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

Разделы

Аффилиация

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