Theorems · Definition · logic and foundations

FirstOrder.Language.Substructure.casesOn

{L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] →
      {motive : L.Substructure M → Sort u_1} →
        (t : L.Substructure M) →
          ((carrier : Set M) →
              (fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier) →
                motive { carrier := carrier, fun_mem := fun_mem }) →
            motive t

Defined in

Mathlib.ModelTheory.Substructures

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

FirstOrder.Language.Structure