Theorems · Definition · logic and foundations

FirstOrder.Language.OrderedStructure.recOn

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

Defined in

Mathlib.ModelTheory.Order

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext

Assumes

FirstOrder.Language.IsOrderedLEFirstOrder.Language.Structure