card_singleton

Mathlib.Data.Finset.Card

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

English

For any a, #{a} = 1.

Русский

Для любого элемента a, #{a} = 1.

LaTeX

$$$\#{a} = 1$$$

Lean4

@[simp, grind =]
theorem card_singleton (a : α) : #{ a } = 1 :=
  Multiset.card_singleton _

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

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

Разделы

Аффилиация

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