card_eq_card_of_rel

Mathlib.Data.Multiset.ZeroCons

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

English

If Rel r s t holds, then card s = card t.

Русский

Если Rel r s t верно, то кардинал s равен кардиналу t.

LaTeX

$$$\text{Rel} \ r\ s\ t \rightarrow \operatorname{card}(s) = \operatorname{card}(t)$$$

Lean4

theorem card_eq_card_of_rel {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) : card s = card t := by
  induction h <;> simp [*]

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

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

Разделы

Аффилиация

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