card_le_card

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.card_le_card

← MathLib Explorer

English

If s ⊆ t and |t| ≤ |s| then s = t.

Русский

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

LaTeX

$$$ hsub : s \\subseteq t \\land hcard : |t| \\le |s| \\Rightarrow s = t $$$

Lean4

theorem card_le_card {s t : Set α} [Fintype s] [Fintype t] (hsub : s ⊆ t) : Fintype.card s ≤ Fintype.card t :=
  Fintype.card_le_of_injective (Set.inclusion hsub) (Set.inclusion_injective hsub)

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

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

Разделы

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

Аффилиация

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