eq_of_superset_of_card_ge

Mathlib.Data.Finset.Card

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

English

If s ⊆ t and #t ≤ #s, then t = s (equivalently, equality follows from the reverse card inequality).

Русский

Если s ⊆ t и #t ≤ #s, то t = s.

LaTeX

$$(hst : s ⊆ t) (hts : #t ≤ #s) : t = s$$

Lean4

theorem eq_of_superset_of_card_ge (hst : s ⊆ t) (hts : #t ≤ #s) : t = s :=
  (eq_of_subset_of_card_le hst hts).symm

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

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

Разделы

Аффилиация

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