eq_of_le_of_card_le

Mathlib.Data.Multiset.Defs

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

← MathLib Explorer

English

If s ≤ t and card t ≤ card s, then s = t.

Русский

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

LaTeX

$$$s\\le t\\Rightarrow \\operatorname{card}(t)\\le \\operatorname{card}(s)\\Rightarrow s=t.$$$

Lean4

theorem eq_of_le_of_card_le {s t : Multiset α} (h : s ≤ t) : card t ≤ card s → s = t :=
  leInductionOn h fun s h₂ => congr_arg _ <| s.eq_of_length_le h₂

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

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

Разделы

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

Аффилиация

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