realize_le — Mathlib

English

For any substructure S of M, the induced structure on S is L-Ordered.

Русский

Для любой подструктуры S структуры M индексированная структура S сохраняет упорядоченность.

LaTeX

$$$ (S : L.Substructure M) \\Rightarrow L.OrderedStructure S $$$

Lean4

@[simp]
theorem realize_le {t₁ t₂ : L.Term (α ⊕ (Fin n))} {v : α → M} {xs : Fin n → M} :
    (t₁.le t₂).Realize v xs ↔ t₁.realize (Sum.elim v xs) ≤ t₂.realize (Sum.elim v xs) := by simp [Term.le]

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