Documentation

Foundation.FirstOrder.Basic.Eq

def Matrix.iget {α : Type u_1} {k : } [Inhabited α] (v : Fin kα) (x : ) :
α
Equations
Instances For
    Instances For
      theorem LO.FirstOrder.Structure.Eq.QuotEq.val_mk {L : LO.FirstOrder.Language} {μ : Type u_1} [LO.FirstOrder.Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {H : M ⊧ₘ* 𝐄𝐐} {n : } {e : Fin nM} {ε : μM} (t : LO.FirstOrder.Semiterm L μ n) :
      LO.FirstOrder.Semiterm.valm (LO.FirstOrder.Structure.Eq.QuotEq H) (fun (i : Fin n) => e i) (fun (i : μ) => ε i) t = LO.FirstOrder.Semiterm.valm M e ε t
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For