covBy_iff

Mathlib.Data.Finset.Grade

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

Lean4

theorem covBy_iff : s ⋖ t ↔ ∃ a, a ::ₘ s = t :=
  ⟨CovBy.exists_multiset_cons, by rintro ⟨a, rfl⟩; exact covBy_cons _ _⟩

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

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

Разделы

Аффилиация

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