eq_iff_card_le_of_subset

Mathlib.Data.Finset.Card

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

English

If s ⊆ t, then #t ≤ #s ↔ s = t.

Русский

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

LaTeX

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

Lean4

theorem eq_iff_card_le_of_subset (hst : s ⊆ t) : #t ≤ #s ↔ s = t :=
  ⟨eq_of_subset_of_card_le hst, (ge_of_eq <| congr_arg _ ·)⟩

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

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

Разделы

Аффилиация

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