mk_equiv_le_embedding

Mathlib.SetTheory.Cardinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_equiv_le_embedding

English

For α, β' one has #(Equiv α β') ≤ #(α ↪ β').

Русский

Для любых α, β' верно #(Equiv α β') ≤ #(α ↪ β').

LaTeX

$$$ #(\\alpha \\simeq \\beta') \\le #(\\alpha \\hookrightarrow \\beta') $$$

Lean4

theorem mk_equiv_le_embedding : #(α ≃ β') ≤ #(α ↪ β') :=
  ⟨⟨_, Equiv.toEmbedding_injective⟩⟩

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

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

Разделы

Аффилиация

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