nonempty_equiv_iff — Mathlib

English

There exists a nonempty equivalence M ≃ N in the empty-language setting if and only if the lifted cardinalities of M and N are equal.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem nonempty_equiv_iff : Nonempty (M ≃[Language.empty] N) ↔ Cardinal.lift.{w'} #M = Cardinal.lift.{w} #N :=
  _root_.trans ⟨Nonempty.map fun f => f.toEquiv, Nonempty.map fun f => { toEquiv := f }⟩ Cardinal.lift_mk_eq'.symm

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