card_le_four

Mathlib.Data.Finset.Card

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

English

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

Русский

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

LaTeX

$$$|\{a,b,c,d\}| \le 4$$$

Lean4

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

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

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

Разделы

Аффилиация

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