Theorems · Definition · logic and foundations

FirstOrder.Language.Substructure.mk.noConfusion

{L : FirstOrder.Language} →
  {M : Type w} →
    {inst : L.Structure M} →
      {P : Sort u_1} →
        {carrier : Set M} →
          {fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier} →
            {carrier' : Set M} →
              {fun_mem' : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier'} →
                { carrier := carrier, fun_mem := fun_mem } = { carrier := carrier', fun_mem := fun_mem' } →
                  (carrier ≍ carrier' → P) → P

Defined in

Mathlib.ModelTheory.Substructures

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms