instOrderedStructureSubtypeMemSubstructure

English

If L is ordered and M has a compatible order structure and its orderLHom is an expansion on M, then M carries an L-OrderedStructure.

Русский

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

LaTeX

$$$ (L.orderLHom.IsExpansionOn M) \\Rightarrow L.OrderedStructure M $$$

Lean4

instance (S : L.Substructure M) : L.OrderedStructure S :=
  ⟨fun x => relMap_leSymb (S.subtype ∘ x)⟩

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