Theorems · Theorem · logic and foundations

FirstOrder.Language.OrderedStructure.relMap_leSymb

∀ {L : FirstOrder.Language} {M : Type w'} {inst : L.IsOrdered} {inst_1 : LE M} {inst_2 : L.Structure M}
  [self : L.OrderedStructure M] (x : Fin 2 → M),
  FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb x ↔ x 0 ≤ x 1

Defined in

Mathlib.ModelTheory.Order

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

FirstOrder.Language.OrderedStructure