Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.ModelType.defaultExpansion_Carrier

∀ {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective)
  [inst : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => φ.onFunction f)]
  [inst_1 : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => φ.onRelation r)] (M : T.ModelType)
  [inst_2 : Inhabited ↑M], ↑(FirstOrder.Language.Theory.ModelType.defaultExpansion h M) = ↑M

Defined in

Mathlib.ModelTheory.Bundled

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableDecidableInhabited