realize_denselyOrdered_iff — Mathlib

English

A model realizes denselyOrderedSentence iff the domain is densely ordered.

Русский

Модель реализует denselyOrderedSentence тогда и только тогда, когда множество плотно упорядочено.

LaTeX

$$$ M \\models L.denselyOrderedSentence \\iff DenselyOrdered M $$$

Lean4

theorem realize_denselyOrdered_iff : M ⊨ L.denselyOrderedSentence ↔ DenselyOrdered M :=
  by
  simp only [denselyOrderedSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_imp,
    BoundedFormula.realize_all, Term.realize_lt, BoundedFormula.realize_ex, BoundedFormula.realize_inf]
  refine ⟨fun h => ⟨fun a b ab => h a b ab⟩, ?_⟩
  intro h a b ab
  exact exists_between ab

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