instModelPartialOrderTheoryOfLinearOrderTheory

English

If M satisfies the linear order theory, then M satisfies the partial order theory.

Русский

Если M удовлетворяет линейной теории порядка, то она удовлетворяет теории частичного порядка.

LaTeX

$$$ (M \\models L.linearOrderTheory) \\Rightarrow (M \\models L.partialOrderTheory) $$$

Lean4

instance [h : M ⊨ L.linearOrderTheory] : M ⊨ L.partialOrderTheory :=
  h.mono (Set.subset_insert _ _)

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