Theorems · Theorem · logic and foundations

FirstOrder.Language.IsExtensionPair.cod

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.IsExtensionPair M N → ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g

Alias of the forward direction of FirstOrder.Language.isExtensionPair_iff_cod.

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure