zero_le

Mathlib.Data.Multiset.ZeroCons

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

English

The zero multiset is less than or equal to any multiset with respect to the natural order.

Русский

Нуль-мультимножество не превышает заданное мультимножество по естественному порядку.

LaTeX

$$$0 \\le s$$$

Lean4

theorem zero_le (s : Multiset α) : 0 ≤ s :=
  Quot.inductionOn s fun l => (nil_sublist l).subperm

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

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

Разделы

Аффилиация

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