nonempty_embedding_iff — Mathlib

English

There exists a nonempty embedding M ↪ N in the empty-language setting if and only if the (cardinal) size of M lifts to at most the lift of N.

Русский

Существует непустое вложение M ↪ N в условиях пустого языка тогда и только если размер M после подъема не превосходит подъем размера N.

LaTeX

$$$\text{Nonempty}(M \hookrightarrow_{\mathrm{Language.empty}} N) \iff \operatorname{lift}^{w'}(|M|) \le \operatorname{lift}^{w}(|N|).$$$

Lean4

@[simp]
theorem nonempty_embedding_iff : Nonempty (M ↪[Language.empty] N) ↔ Cardinal.lift.{w'} #M ≤ Cardinal.lift.{w} #N :=
  _root_.trans ⟨Nonempty.map fun f => f.toEmbedding, Nonempty.map StrongHomClass.toEmbedding⟩ Cardinal.lift_mk_le'.symm

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