Theorems · Definition · logic and foundations

FirstOrder.Language.Prestructure.recOn

{L : FirstOrder.Language} →
  {M : Type u_1} →
    {s : Setoid M} →
      {motive : L.Prestructure s → Sort u} →
        (t : L.Prestructure s) →
          ((toStructure : L.Structure M) →
              (fun_equiv :
                  ∀ {n : ℕ} {f : L.Functions n} (x y : Fin n → M),
                    x ≈ y → FirstOrder.Language.Structure.funMap f x ≈ FirstOrder.Language.Structure.funMap f y) →
                (rel_equiv :
                    ∀ {n : ℕ} {r : L.Relations n} (x y : Fin n → M),
                      x ≈ y → FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r y) →
                  motive { toStructure := toStructure, fun_equiv := fun_equiv, rel_equiv := rel_equiv }) →
            motive t

Defined in

Mathlib.ModelTheory.Quotients

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms