instOrderedStructureOfOrderOfIsExpansionOnOrderLHom

English

If L is ordered and M has an order structure, then the orderLHom is an expansion on M.

Русский

Если L упорядочен и M имеет структуру порядка, то orderLHom является расширением на M.

LaTeX

$$$ [L.OrderedStructure M] [L.order.Structure M] \\Rightarrow LHom.IsExpansionOn (orderLHom L) M $$$

Lean4

instance [Language.order.Structure M] [Language.order.OrderedStructure M] [(orderLHom L).IsExpansionOn M] :
    L.OrderedStructure M where
  relMap_leSymb x := by rw [← orderLHom_leSymb L, LHom.IsExpansionOn.map_onRelation, relMap_leSymb]

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