card_strictMono

Mathlib.Data.Finset.Card

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

English

The function that assigns to a finite set its cardinality is strictly monotone with respect to inclusion.

Русский

Функция, сопоставляющая кардинал множества, строго монотонна по включению.

LaTeX

$$$\\text{StrictMono}(\\text{card}|_{\ \mathrm{Finset}\,\\alpha})$$$

Lean4

theorem card_strictMono : StrictMono (card : Finset α → ℕ) := fun _ _ ↦ card_lt_card

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

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

Разделы

Аффилиация

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