card_pair

Mathlib.Data.Multiset.ZeroCons

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

English

The cardinality of a two-element multiset {a,b} is 2.

Русский

Кардинал мультимножества {a,b} равен 2.

LaTeX

$$card({a,b}) = 2$$

Lean4

theorem card_pair (a b : α) : card { a, b } = 2 := by rw [insert_eq_cons, card_cons, card_singleton]

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

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

Разделы

Аффилиация

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