card_multiset

Mathlib.Data.Finset.Grade

URI: https://scilib.ai/kg/mathlib#CovBy.card_multiset

← MathLib Explorer

English

If s is covered by t, then card(s) is covered by card(t) in the natural numbers.

Русский

Если s покрыто t, тогда card(s) покрыто card(t) в натуральных числах.

LaTeX

$$$ \operatorname{card}(s) \; \covBy\; \operatorname{card}(t) $$$

Lean4

theorem _root_.CovBy.card_multiset (h : s ⋖ t) : card s ⋖ card t := by obtain ⟨a, rfl⟩ := h.exists_multiset_cons;
  rw [card_cons]; exact covBy_succ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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