out_embedding — Mathlib

English

For cardinals c, c', we have c ≤ c' if and only if the quotient-out representations satisfy a nonempty embedding.

Русский

Для кардиналов c, c' выполнение c ≤ c' эквивалентно существованию непустого вложения между их представлениями через quotient-out.

LaTeX

$$$$ c \\le c' \\iff \\mathrm{Nonempty}(c.\\mathrm{out} \\hookrightarrow c'.\\mathrm{out}). $$$$

Lean4

theorem out_embedding {c c' : Cardinal} : c ≤ c' ↔ Nonempty (c.out ↪ c'.out) := by
  conv_lhs => rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]

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