Theorems · Theorem · logic and foundations

FirstOrder.Language.PartialEquiv.le_iff

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N},
  f ≤ g ↔
    ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom),
        (FirstOrder.Language.Substructure.inclusion cod_le_cod) (f.toEquiv x) =
          g.toEquiv ((FirstOrder.Language.Substructure.inclusion dom_le_dom) x)

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure