orderLHom_leSymb — Mathlib

English

Let L be an ordered language. The relation symbol for the order, leSymb, is preserved by the order-homomorphism. In particular, the induced relation on leSymb agrees with the original leSymb.

Русский

Пусть L — упорядоченный язык. Отображение порядка сохраняет символ отношения порядка leSymb: полученное отношение равняется исходному leSymb.

LaTeX

$$$ (orderLHom L).onRelation leSymb = (leSymb : L.Relations 2) $$$

Lean4

@[simp]
theorem orderLHom_leSymb : (orderLHom L).onRelation leSymb = (leSymb : L.Relations 2) :=
  rfl

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