card_le_five

Mathlib.Data.Finset.Card

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

English

For any a, b, c, d, e, the set {a, b, c, d, e} contains at most five distinct elements.

Русский

Пусть a, b, c, d, e — произвольные элементы; множество {a, b, c, d, e} содержит не более пяти элементов.

LaTeX

$$$|\{a,b,c,d,e\}| \le 5$$$

Lean4

theorem card_le_five : #{ a, b, c, d, e } ≤ 5 :=
  (card_insert_le _ _).trans (Nat.succ_le_succ card_le_four)

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

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

Разделы

Аффилиация

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