Theorems · Theorem · logic and foundations

FirstOrder.Language.empty.nonempty_equiv_iff

∀ {M : Type w} {N : Type w'} [inst : FirstOrder.Language.empty.Structure M]
  [inst_1 : FirstOrder.Language.empty.Structure N],
  Nonempty (FirstOrder.Language.empty.Equiv M N) ↔
    Cardinal.lift.{w', w} (Cardinal.mk M) = Cardinal.lift.{w, w'} (Cardinal.mk N)

Defined in

Mathlib.ModelTheory.Basic

Cited by

1 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure