card_finset

Mathlib.Data.Finset.Grade

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

English

If Finset s is covered by Finset t, then their cardinals satisfy s.card ⋖ t.card.

Русский

Если Finset s покрыто Finset t, то их кардинальности удовлетворяют s.card ⋖ t.card.

LaTeX

$$$ s.card \covBy t.card $$$

Lean4

theorem _root_.CovBy.card_finset (h : s ⋖ t) : s.card ⋖ t.card :=
  (val_covBy_val.2 h).card_multiset

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

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

Разделы

Аффилиация

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