card_le_six

Mathlib.Data.Finset.Card

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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