univ_fin2

Mathlib.LinearAlgebra.AffineSpace.Combination

URI: https://scilib.ai/kg/mathlib#Finset.univ_fin2

English

Let Fin 2 be the two-element set {0,1}. The universal finite set of Fin 2 is exactly {0,1}.

Русский

Пусть Fin 2 — множество из двух элементов {0,1}. Общее множество Fin 2 совпадает с {0,1}.

LaTeX

$$$\\\\mathrm{univ}_{\\\\mathrm{Fin}(2)} = \\{0,1\\\\}$$$

Lean4

theorem univ_fin2 : (univ : Finset (Fin 2)) = {0, 1} :=
  rfl

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

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

Разделы

Аффилиация

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