dlo_isComplete — Mathlib

English

The theory of dense linear orders is complete (ℵ0-complete).

Русский

Теория плотных линейных порядков полна (ℵ0-полнa).

LaTeX

$$$ \text{DLO IsComplete} $$$

Lean4

/-- The theory of dense linear orders is `ℵ₀`-complete. -/
theorem dlo_isComplete : Language.order.dlo.IsComplete :=
  aleph0_categorical_dlo.{0}.isComplete ℵ₀ _ le_rfl (by simp [one_le_aleph0])
    ⟨by
      letI : Language.order.Structure ℚ := orderStructure ℚ
      exact Theory.ModelType.of _ ℚ⟩
    fun _ => inferInstance

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