eq_iff_card_ge_of_superset

Mathlib.Data.Finset.Card

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

English

For s ⊆ t, #t ≤ #s ↔ t = s; a reformulation of the previous equivalence.

Русский

Для s ⊆ t: #t ≤ #s ⇔ t = s.

LaTeX

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

Lean4

theorem eq_iff_card_ge_of_superset (hst : s ⊆ t) : #t ≤ #s ↔ t = s :=
  (eq_iff_card_le_of_subset hst).trans eq_comm

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

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

Разделы

Аффилиация

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