Theorems · Definition · logic and foundations

FirstOrder.Language.Theory.ModelType.casesOn

{L : FirstOrder.Language} →
  {T : L.Theory} →
    {motive : T.ModelType → Sort u_1} →
      (t : T.ModelType) →
        ((Carrier : Type w) →
            [struc : L.Structure Carrier] →
              [is_model : Carrier ⊨ T] →
                [nonempty' : Nonempty Carrier] →
                  motive { Carrier := Carrier, struc := struc, is_model := is_model, nonempty' := nonempty' }) →
          motive t

Defined in: Mathlib.ModelTheory.Bundled
Cited by: 4 results in Mathlib
Foundations: Depth 10 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

FirstOrder.Languagestatement and proof · cited by 1,084
FirstOrder.Language.Structurestatement and proof · cited by 775
FirstOrder.Language.Theorystatement and proof · cited by 154
FirstOrder.Language.Theory.Modelstatement and proof · cited by 67
FirstOrder.Language.Theory.ModelTypestatement and proof · cited by 62

Cited by6

Results whose statement or proof uses this declaration.

FirstOrder.Field.ACF_isCompleteproof · cited by 3
FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realizeproof · cited by 2
FirstOrder.Field.ACF_categoricalproof · cited by 1
FirstOrder.Language.Theory.CompleteType.not_mem_iffproof · cited by 1
FirstOrder.Language.Theory.ModelType.noConfusionproof · cited by 0
FirstOrder.Language.Theory.ModelType.noConfusionTypeproof · cited by 0