Theorems · Theorem · logic and foundations

FirstOrder.Language.Structure.ext

∀ {L : FirstOrder.Language} {M : Type w} {x y : L.Structure M},
  @FirstOrder.Language.Structure.funMap L M x = @FirstOrder.Language.Structure.funMap L M y →
    @FirstOrder.Language.Structure.RelMap L M x = @FirstOrder.Language.Structure.RelMap L M y → x = y

Defined in

Mathlib.ModelTheory.Basic

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses no axioms