Theorems · Theorem · logic and foundations

FirstOrder.Language.PartialEquiv.ext_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 ↔
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure