mk_embedding_eq_arrow_of_le

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

If α is infinite and #β ≤ #α, then #(β ↪ α) = #(β → α).

Русский

Если α бесконечен и #β ≤ #α, то #(β ↪ α) = #(β → α).

LaTeX

$$$ #(β \\hookrightarrow α) = #(β \\to α) $$$

Lean4

theorem mk_embedding_eq_arrow_of_le (le : #β ≤ #α) : #(β ↪ α) = #(β → α) :=
  mk_embedding_eq_arrow_of_lift_le (lift_le.mpr le)

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

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

Разделы

Аффилиация

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