Documentation

Arithmetization.Definability.BoundedBoldface

class LO.FirstOrder.Arith.Bounded {V : Type u_2} [LO.ORingStruc V] {k : } (f : (Fin kV)V) :
Instances
    theorem LO.FirstOrder.Arith.Bounded.bounded {V : Type u_2} [LO.ORingStruc V] {k : } {f : (Fin kV)V} [self : LO.FirstOrder.Arith.Bounded f] :
    ∃ (t : LO.FirstOrder.Semiterm ℒₒᵣ V k), ∀ (v : Fin kV), f v LO.FirstOrder.Semiterm.valm V v id t
    @[reducible, inline]
    abbrev LO.FirstOrder.Arith.Bounded₁ {V : Type u_2} [LO.ORingStruc V] (f : VV) :
    Equations
    Instances For
      @[reducible, inline]
      abbrev LO.FirstOrder.Arith.Bounded₂ {V : Type u_2} [LO.ORingStruc V] (f : VVV) :
      Equations
      Instances For
        @[reducible, inline]
        abbrev LO.FirstOrder.Arith.Bounded₃ {V : Type u_2} [LO.ORingStruc V] (f : VVVV) :
        Equations
        Instances For
          Equations
          • =
          @[simp]
          theorem LO.FirstOrder.Arith.Bounded.var {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (i : Fin k) :
          LO.FirstOrder.Arith.Bounded fun (v : Fin kV) => v i
          @[simp]
          theorem LO.FirstOrder.Arith.Bounded.const {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (c : V) :
          LO.FirstOrder.Arith.Bounded fun (x : Fin kV) => c
          @[simp]
          theorem LO.FirstOrder.Arith.Bounded.term_retraction {n : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (t : LO.FirstOrder.Semiterm ℒₒᵣ V n) (e : Fin nFin k) :
          LO.FirstOrder.Arith.Bounded fun (v : Fin kV) => LO.FirstOrder.Semiterm.valm V (fun (x : Fin n) => v (e x)) id t
          theorem LO.FirstOrder.Arith.Bounded.retraction {n : } {V : Type u_2} [LO.ORingStruc V] {k : } {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.Bounded f) (e : Fin kFin n) :
          LO.FirstOrder.Arith.Bounded fun (v : Fin nV) => f fun (i : Fin k) => v (e i)
          theorem LO.FirstOrder.Arith.Bounded.comp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {l : } {k : } {f : (Fin lV)V} {g : Fin l(Fin kV)V} (hf : LO.FirstOrder.Arith.Bounded f) (hg : ∀ (i : Fin l), LO.FirstOrder.Arith.Bounded (g i)) :
          LO.FirstOrder.Arith.Bounded fun (v : Fin kV) => f fun (x : Fin l) => g x v
          theorem LO.FirstOrder.Arith.Bounded₁.comp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {f : VV} {k : } {g : (Fin kV)V} (hf : LO.FirstOrder.Arith.Bounded₁ f) (hg : LO.FirstOrder.Arith.Bounded g) :
          LO.FirstOrder.Arith.Bounded fun (v : Fin kV) => f (g v)
          theorem LO.FirstOrder.Arith.Bounded₂.comp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {f : VVV} {k : } {g₁ : (Fin kV)V} {g₂ : (Fin kV)V} (hf : LO.FirstOrder.Arith.Bounded₂ f) (hg₁ : LO.FirstOrder.Arith.Bounded g₁) (hg₂ : LO.FirstOrder.Arith.Bounded g₂) :
          LO.FirstOrder.Arith.Bounded fun (v : Fin kV) => f (g₁ v) (g₂ v)
          theorem LO.FirstOrder.Arith.Bounded₃.comp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {f : VVVV} {k : } {g₁ : (Fin kV)V} {g₂ : (Fin kV)V} {g₃ : (Fin kV)V} (hf : LO.FirstOrder.Arith.Bounded₃ f) (hg₁ : LO.FirstOrder.Arith.Bounded g₁) (hg₂ : LO.FirstOrder.Arith.Bounded g₂) (hg₃ : LO.FirstOrder.Arith.Bounded g₃) :
          LO.FirstOrder.Arith.Bounded fun (v : Fin kV) => f (g₁ v) (g₂ v) (g₃ v)
          Equations
          • =
          Equations
          • =
          @[reducible, inline]
          Equations
          Instances For
            @[reducible, inline]
            abbrev LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ {V : Type u_2} [LO.ORingStruc V] (f : VVV) :
            Equations
            Instances For
              @[reducible, inline]
              abbrev LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ {V : Type u_2} [LO.ORingStruc V] (f : VVVV) :
              Equations
              Instances For
                theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction.retraction {n : } {V : Type u_2} [LO.ORingStruc V] {k : } {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (e : Fin kFin n) :
                LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin nV) => f fun (i : Fin k) => v (e i)
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_blt {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : .Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                .Boldface fun (v : Fin kV) => x < f v, P v x
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_blt {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : .Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                .Boldface fun (v : Fin kV) => x < f v, P v x
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_ble {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : .Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                .Boldface fun (v : Fin kV) => xf v, P v x
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_ble {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : .Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                .Boldface fun (v : Fin kV) => xf v, P v x
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_blt_zero {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : { Γ := Γ, rank := 0 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                { Γ := Γ, rank := 0 }.Boldface fun (v : Fin kV) => x < f v, P v x
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_blt_zero {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : { Γ := Γ, rank := 0 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                { Γ := Γ, rank := 0 }.Boldface fun (v : Fin kV) => x < f v, P v x
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_ble_zero {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : { Γ := Γ, rank := 0 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                { Γ := Γ, rank := 0 }.Boldface fun (v : Fin kV) => xf v, P v x
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_ble_zero {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : { Γ := Γ, rank := 0 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                { Γ := Γ, rank := 0 }.Boldface fun (v : Fin kV) => xf v, P v x
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_vec_le_boldfaceBoundedFunction {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {l : } {k : } {p : Fin l(Fin kV)V} {P : (Fin kV)(Fin lV)Prop} (pp : ∀ (i : Fin l), LO.FirstOrder.Arith.BoldfaceBoundedFunction (p i)) (hP : .Boldface fun (w : Fin (k + l)V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) :
                .Boldface fun (v : Fin kV) => wfun (x : Fin l) => p x v, P v w
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.substitution_boldfaceBoundedFunction {k : } {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {P : (Fin kV)Prop} {l : } {f : Fin k(Fin lV)V} (hP : .Boldface P) (hf : ∀ (i : Fin k), LO.FirstOrder.Arith.BoldfaceBoundedFunction (f i)) :
                .Boldface fun (z : Fin lV) => P fun (x : Fin k) => f x z
                theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction.of_iff {V : Type u_2} [LO.ORingStruc V] {k : } {f : (Fin kV)V} {g : (Fin kV)V} (H : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) (h : ∀ (v : Fin kV), f v = g v) :
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₁ {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : VProp} {f : (Fin kV)V} [hP : -Predicate P] (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) :
                .Boldface fun (v : Fin kV) => P (f v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₂ {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {R : VVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} [hR : -Relation R] (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) :
                .Boldface fun (v : Fin kV) => R (f₁ v) (f₂ v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₃ {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {R : VVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} [hR : -Relation₃ R] (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) (hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃) :
                .Boldface fun (v : Fin kV) => R (f₁ v) (f₂ v) (f₃ v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₄ {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {R : VVVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} {f₄ : (Fin kV)V} [hR : -Relation₄ R] (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) (hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃) (hf₄ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₄) :
                .Boldface fun (v : Fin kV) => R (f₁ v) (f₂ v) (f₃ v) (f₄ v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₁_zero {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {Γ : LO.SigmaPiDelta} {k : } {P : VProp} {f : (Fin kV)V} [hP : { Γ := Γ, rank := 0 }-Predicate P] (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) :
                { Γ := Γ, rank := 0 }.Boldface fun (v : Fin kV) => P (f v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₂_zero {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {Γ : LO.SigmaPiDelta} {k : } {R : VVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} [hR : { Γ := Γ, rank := 0 }-Relation R] (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) :
                { Γ := Γ, rank := 0 }.Boldface fun (v : Fin kV) => R (f₁ v) (f₂ v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₃_zero {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {Γ : LO.SigmaPiDelta} {k : } {R : VVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} [hR : { Γ := Γ, rank := 0 }-Relation₃ R] (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) (hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃) :
                { Γ := Γ, rank := 0 }.Boldface fun (v : Fin kV) => R (f₁ v) (f₂ v) (f₃ v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₄_zero {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {Γ : LO.SigmaPiDelta} {k : } {R : VVVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} {f₄ : (Fin kV)V} [hR : { Γ := Γ, rank := 0 }-Relation₄ R] (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) (hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃) (hf₄ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₄) :
                { Γ := Γ, rank := 0 }.Boldface fun (v : Fin kV) => R (f₁ v) (f₂ v) (f₃ v) (f₄ v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.bcomp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {l : } {k : } {F : (Fin lV)V} {f : Fin l(Fin kV)V} (hF : .BoldfaceFunction F) (hf : ∀ (i : Fin l), LO.FirstOrder.Arith.BoldfaceBoundedFunction (f i)) :
                .BoldfaceFunction fun (v : Fin kV) => F fun (x : Fin l) => f x v
                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.bcomp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {F : VV} {f : (Fin kV)V} (hF : -Function₁ F) (hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f) :
                .BoldfaceFunction fun (v : Fin kV) => F (f v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.bcomp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {F : VVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} (hF : -Function₂ F) (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) :
                .BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v)
                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.bcomp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {F : VVVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} (hF : -Function₃ F) (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) (hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃) :
                .BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v)
                theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction₂.comp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {F : VVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} (hF : LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ F) (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) :
                LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin kV) => F (f₁ v) (f₂ v)
                theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction₃.comp {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {F : VVVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} (hF : LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ F) (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) (hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃) :
                LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v)
                theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction.comp₂ {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {F : VVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} [hFb : LO.FirstOrder.Arith.Bounded₂ F] [hFd : 𝚺₀-Function₂ F] (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) :
                LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin kV) => F (f₁ v) (f₂ v)
                theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction.comp₃ {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {F : VVVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} [hFb : LO.FirstOrder.Arith.Bounded₃ F] [hFd : 𝚺₀-Function₃ F] (hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁) (hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂) (hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃) :
                LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v)
                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