Theorems · Theorem · logic and foundations

FirstOrder.Language.DirectLimit.Equiv_isup_of_apply

∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  {M : Type u_1} [inst_3 : L.Structure M] (S : ι →o L.Substructure M) {i : ι} (x : ↥(S i)),
  (FirstOrder.Language.DirectLimit.Equiv_iSup S)
      ((FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x))
          (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i)
        x) =
    (FirstOrder.Language.Substructure.inclusion ⋯) x

Defined in

Mathlib.ModelTheory.DirectLimit

Cited by

0 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderNonemptyIsDirectedOrderFirstOrder.Language.Structure