Theorems · Theorem · logic and foundations

FirstOrder.Language.dlo_isExtensionPair

∀ (M : Type w) [inst : FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.linearOrderTheory]
  (N : Type w') [inst_2 : FirstOrder.Language.order.Structure N] [N ⊨ FirstOrder.Language.order.dlo] [Nonempty N],
  FirstOrder.Language.order.IsExtensionPair M N

Defined in

Mathlib.ModelTheory.Order

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Theory.ModelFirstOrder.Language.StructureFirstOrder.Language.Theory.ModelNonempty