Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.typeOf.congr_simp

∀ {L : FirstOrder.Language} (T : L.Theory) {α : Type w} {M : Type w'} [inst : L.Structure M] [inst_1 : Nonempty M]
  [inst_2 : M ⊨ T] (v v_1 : α → M), v = v_1 → T.typeOf v = T.typeOf v_1

Defined in

Mathlib.ModelTheory.Types

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureNonemptyFirstOrder.Language.Theory.Model