card_pair_eq_one_or_two

Mathlib.Data.Finset.Card

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

English

For any a, b, the set {a, b} has either one or two elements.

Русский

Для любых a, b множество {a, b} содержит либо один, либо два элемента.

LaTeX

$$$|\{a,b\}| = 1 \lor |\{a,b\}| = 2$$$

Lean4

@[simp]
theorem card_pair_eq_one_or_two : #{ a, b } = 1 ∨ #{ a, b } = 2 := by grind

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

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

Разделы

Аффилиация

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