lift_mk_le — Mathlib

English

The lift operation preserves a cardinal inequality via embeddings: lift a ≤ lift b whenever there exists an embedding a ↪ b.

Русский

Применение lift сохраняет неравенство кардиналов через вложения: lift a ≤ lift b тогда и только если существует вложение a ↪ b.

LaTeX

$$$$ \\text{lift}\\,a \\le \\text{lift}\\,b \\iff \\text{Nonempty}(f:\\alpha \\hookrightarrow \\beta). $$$$

Lean4

theorem lift_mk_le {α : Type v} {β : Type w} : lift.{max u w} #α ≤ lift.{max u v} #β ↔ Nonempty (α ↪ β) :=
  ⟨fun ⟨f⟩ => ⟨Embedding.congr Equiv.ulift Equiv.ulift f⟩, fun ⟨f⟩ =>
    ⟨Embedding.congr Equiv.ulift.symm Equiv.ulift.symm f⟩⟩

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