grade_multiset_eq

Mathlib.Data.Finset.Grade

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

English

For any Finset s, the grade of s in the multiset grading equals the underlying multiset s.1.

Русский

Для любого Finset s грань по мультсетной градации равна базовой мультисетке s.1.

LaTeX

$$$ \operatorname{grade}(\operatorname{Multiset} \alpha)\, s = s.1 $$$

Lean4

@[simp]
theorem grade_multiset_eq (s : Finset α) : grade (Multiset α) s = s.1 :=
  rfl

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

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

Разделы

Аффилиация

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