eq_of_subset_of_encard_le

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.Finite.eq_of_subset_of_encard_le

← MathLib Explorer

English

Let S be finite. If S ⊆ T and T.encard ≤ S.encard, then S = T.

Русский

Пусть S конечен. Если S ⊆ T и T.encard ≤ S.encard, тогда S = T.

LaTeX

$$$\operatorname{Finite}(S) \Rightarrow (S \subseteq T \land T.encard \le S.encard \Rightarrow S = T)$$$

Lean4

theorem eq_of_subset_of_encard_le (hs : s.Finite) (hst : s ⊆ t) (hts : t.encard ≤ s.encard) : s = t :=
  (hs.finite_of_encard_le hts).eq_of_subset_of_encard_le' hst hts

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

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

Разделы

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

Аффилиация

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