mk_embedding_eq_zero_iff_lt — Mathlib

English

For α, β types, the cardinal of embeddings α ↪ β is zero iff α ↪ β is empty, i.e., α ≃ β has no embedding when β is too small.

Русский

Кардинал вложений α ↪ β равен нулю тогда и только тогда, когда вложений нет.

LaTeX

$$$ #(α \\hookrightarrow β) = 0 \\iff #β < #α $$$

Lean4

theorem mk_embedding_eq_zero_iff_lt : #(α ↪ β) = 0 ↔ #β < #α := by rw [mk_embedding_eq_zero_iff_lift_lt, lift_lt]

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