grade_eq

Mathlib.Data.Finset.Grade

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

English

The natural-number grade of a Finset s equals its cardinality.

Русский

Градация по натуральным числам Finset s равна его кардинальности.

LaTeX

$$$ \text{grade} \; \mathbb{N} \; s = |s| $$$

Lean4

@[simp]
theorem grade_eq (s : Finset α) : grade ℕ s = s.card :=
  rfl

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

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

Разделы

Аффилиация

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