noTopOrder_of_dlo — Mathlib

English

For ordered L, L.OrderedStructure M holds iff LHom.IsExpansionOn (orderLHom L) M holds.

Русский

Для упорядоченного L выполнение L.OrderedStructure M эквивалентно тому, что LHom.IsExpansionOn (orderLHom L) M выполняется.

LaTeX

$$$ L.OrderedStructure M \\iff LHom.IsExpansionOn (orderLHom L) M $$$

Lean4

theorem noTopOrder_of_dlo [M ⊨ L.dlo] : NoTopOrder M :=
  realize_noTopOrder_iff.1
    (L.dlo.realize_sentence_of_mem
      (by simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or]))

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