Theorems · Theorem · logic and foundations

FirstOrder.Language.IsFraisseLimit.isFraisse

∀ {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled L.Structure)) {M : Type w} [inst : L.Structure M]
  [inst_1 : Countable ((l : ℕ) × L.Functions l)] [inst_2 : Countable M],
  FirstOrder.Language.IsFraisseLimit K M → FirstOrder.Language.IsFraisse K

If a class has a Fraïssé limit, it must be Fraïssé.

Defined in

Mathlib.ModelTheory.Fraisse

Cited by

2 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureCountableCountable