realize_noTopOrder_iff — Mathlib

English

A model satisfies noTopOrderSentence iff NoTopOrder holds in the domain.

Русский

Модель удовлетворяет noTopOrderSentence тогда и только тогда, когда в множестве нет верхнего элемента.

LaTeX

$$$ M \\models L.noTopOrderSentence \\iff NoTopOrder M $$$

Lean4

theorem realize_noTopOrder_iff : M ⊨ L.noTopOrderSentence ↔ NoTopOrder M :=
  by
  simp only [noTopOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
    BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize_le]
  refine ⟨fun h => ⟨fun a => h a⟩, ?_⟩
  intro h a
  exact exists_not_le a

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