Theorems · Theorem · logic and foundations

FirstOrder.Language.PartialEquiv.ext

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N} (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, ⋯⟩)) → f = g

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

3 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure