card_lt_card

Mathlib.Data.Multiset.Defs

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

← MathLib Explorer

English

If s < t then card(s) < card(t).

Русский

Если s < t, то card(s) < card(t).

LaTeX

$$$s

Lean4

@[gcongr]
theorem card_lt_card {s t : Multiset α} (h : s < t) : card s < card t :=
  lt_of_not_ge fun h₂ => _root_.ne_of_lt h <| eq_of_le_of_card_le (le_of_lt h) h₂

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

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

Разделы

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

Аффилиация

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