orderedStructure_iff — Mathlib

English

Equivalence between L.OrderedStructure M and LHom.IsExpansionOn (orderLHom L) M.

Русский

Эквивалентность между L.OrderedStructure M и LHom.IsExpansionOn (orderLHom L) M.

LaTeX

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

Lean4

@[simp]
theorem orderedStructure_iff [LE M] [Language.order.Structure M] [Language.order.OrderedStructure M] :
    L.OrderedStructure M ↔ LHom.IsExpansionOn (orderLHom L) M :=
  ⟨fun _ => inferInstance, fun _ => inferInstance⟩

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