Theorems · Theorem · logic and foundations

FirstOrder.Language.empty.nonempty_embedding_iff

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

Defined in: Mathlib.ModelTheory.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 25 from the axioms · uses propext, Quot.sound
Assumes: FirstOrder.Language.Structure FirstOrder.Language.Structure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cardinalstatement · cited by 2,598
Cardinal.mkstatement · cited by 942
FirstOrder.Language.Structurestatement and proof · cited by 775
Cardinal.liftstatement · cited by 583
FirstOrder.Language.Embeddingstatement and proof · cited by 128
transproof · cited by 111
Nonempty.mapproof · cited by 101
Cardinal.lift_mk_le'proof · cited by 20
FirstOrder.Language.emptystatement and proof · cited by 8
FirstOrder.Language.Embedding.toEmbeddingproof · cited by 5
FirstOrder.Language.StrongHomClass.toEmbeddingproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.