Theorems · Definition · logic and foundations

FirstOrder.Language.Structure.Sigma

{L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      {G : ι → Type w} →
        [inst_1 : (i : ι) → L.Structure (G i)] → ((i j : ι) → i ≤ j → L.Embedding (G i) (G j)) → Type (max v w)

Alias for Σ i, G i. Instead of Σ i, G i, we use the alias Language.Structure.Sigma which depends on f. This way, Lean can infer what L and f are in the Setoid instance. Otherwise we have a "cannot find synthesization order" error. See also the discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/local.20instance.20cannot.20find.20synthesization.20order.20in.20porting

Defined in

Mathlib.ModelTheory.DirectLimit

Cited by

15 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

PreorderFirstOrder.Language.Structure