card_lt_card

Mathlib.Data.Finset.Card

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

English

If s is a strict subset of t, then the cardinality of s is strictly less than that of t.

Русский

Если s является строгим подмножеством t, то кардинал s строго меньше кардинала t.

LaTeX

$$$s \\subset t \\Rightarrow #s < #t$$$

Lean4

@[gcongr]
nonrec theorem card_lt_card (h : s ⊂ t) : #s < #t :=
  card_lt_card <| val_lt_iff.2 h

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

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

Разделы

Аффилиация

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