realize_noBotOrder_iff — Mathlib

English

A model realizes noBottom ordering iff NoBotOrder holds in M.

Русский

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

LaTeX

$$$ M \\models L.noBotOrderSentence \\iff NoBotOrder M $$$

Lean4

theorem realize_noBotOrder_iff : M ⊨ L.noBotOrderSentence ↔ NoBotOrder M :=
  by
  simp only [noBotOrderSentence, 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_ge a

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