card_pair

Mathlib.Data.Finset.Card

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

English

If a ≠ b, then the set {a, b} has two elements.

Русский

Если a ≠ b, то множество {a, b} содержит два элемента.

LaTeX

$$$a \neq b \Rightarrow |\{a,b\}| = 2$$$

Lean4

theorem card_pair (h : a ≠ b) : #{ a, b } = 2 := by simp [h]

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

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

Разделы

Аффилиация

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