ncard_strictMono

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.ncard_strictMono

English

Let α be finite. If s ⊊ t are subsets of α, then ncard(s) < ncard(t).

Русский

Пусть α конечен. Если s ⊊ t и оба подмножества α, то ncard(s) < ncard(t).

LaTeX

$$$$ [\mathrm{Finite}(\alpha)]\; \forall s,t \subseteq \alpha,\ s \subsetneq t \Rightarrow |s| < |t| $$$$

Lean4

theorem ncard_strictMono [Finite α] : @StrictMono (Set α) _ _ _ ncard := fun _ _ h ↦ ncard_lt_ncard h

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

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

Разделы

Аффилиация

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