mk_embedding_le_arrow — Mathlib

English

For α, β, there is an embedding from α into β iff there is a function from α to β; thus #(α ↪ β) ≤ #(α → β).

Русский

Существует вложение α ↪ β тогда и только тогда существует функция α → β; следовательно #(α ↪ β) ≤ #(α → β).

LaTeX

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

Lean4

theorem mk_embedding_le_arrow : #(α ↪ β') ≤ #(α → β') :=
  ⟨⟨_, DFunLike.coe_injective⟩⟩

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