isFraisse_finite — Mathlib

English

The class of finite structures in the empty language is Fraïssé.

Русский

Класс конечных структур пустого языка является Фраиссé.

LaTeX

$$$IsFraisse(\{S : Bundled(Language.empty.Structure) \mid Finite S\})$$$

Lean4

/-- The class of finite structures in the empty language is Fraïssé. -/
theorem isFraisse_finite : IsFraisse {S : Bundled.{w} Language.empty.Structure | Finite S} :=
  by
  have : Language.empty.Structure (ULift ℕ : Type w) := emptyStructure
  exact (isFraisseLimit_of_countable_infinite (ULift ℕ)).isFraisse

Похожие утверждения