card_le_two

Mathlib.Data.Finset.Card

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

English

The finite set {a, b} has at most two elements, i.e., # {a, b} ≤ 2.

Русский

У множества {a, b} не более двух элементов: # {a, b} ≤ 2.

LaTeX

$$≤ {a, b} ≤ 2$$

Lean4

theorem card_le_two : #{ a, b } ≤ 2 :=
  card_insert_le _ _

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

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

Разделы

Аффилиация

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