Documentation

Arithmetization.ISigmaOne.HFS.Seq

Sequence #

def LO.Arith.Seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
Equations
Instances For
    Equations
    • =
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • =
        Equations
        • =
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def LO.Arith.lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
          V
          Equations
          Instances For
            @[simp]
            theorem LO.Arith.lh_bound {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • =
              Equations
              • =
              theorem LO.Arith.Seq.exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) :
              ∃ (y : V), x, y s
              theorem LO.Arith.Seq.nth_exists_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) :
              ∃! y : V, x, y s
              def LO.Arith.Seq.nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) :
              V
              Equations
              Instances For
                @[simp]
                theorem LO.Arith.Seq.nth_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) :
                x, h.nth hx s
                theorem LO.Arith.Seq.nth_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} {y : V} (hx : x < LO.Arith.lh s) (hy : x, y s) :
                y = h.nth hx
                @[simp]
                theorem LO.Arith.Seq.nth_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) :
                h.nth hx < s
                theorem LO.Arith.Seq.lt_lh_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {i : V} {x : V} (hix : i, x s) :
                def LO.Arith.seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (x : V) :
                V
                Equations
                Instances For
                  def LO.Arith.znth_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (i : V) :
                  ∃! x : V, (LO.Arith.Seq s i < LO.Arith.lh si, x s) (¬(LO.Arith.Seq s i < LO.Arith.lh s)x = 0)
                  Equations
                  • =
                  Instances For
                    def LO.Arith.znth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (i : V) :
                    V
                    Equations
                    Instances For
                      theorem LO.Arith.Seq.znth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {i : V} (h : LO.Arith.Seq s) (hi : i < LO.Arith.lh s) :
                      i, LO.Arith.znth s i s
                      theorem LO.Arith.Seq.znth_eq_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {s : V} {i : V} (h : LO.Arith.Seq s) (hi : i, x s) :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • =
                        Equations
                        • =
                        @[simp]
                        theorem LO.Arith.Seq.subset_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (x : V) :
                        s s ⁀' x
                        theorem LO.Arith.Seq.lt_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (hs : LO.Arith.Seq s) (x : V) :
                        s < s ⁀' x
                        @[simp]
                        theorem LO.Arith.Seq.mem_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (x : V) :
                        LO.Arith.lh s, x s ⁀' x
                        theorem LO.Arith.Seq.seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) (x : V) :
                        @[simp]
                        theorem LO.Arith.Seq.lh_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) {s : V} (h : LO.Arith.Seq s) :
                        theorem LO.Arith.mem_seqCons_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {x : V} {z : V} {s : V} :
                        i, x s ⁀' z i = LO.Arith.lh s x = z i, x s
                        @[simp]
                        theorem LO.Arith.lh_mem_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (z : V) :
                        LO.Arith.lh s, z s ⁀' z
                        @[simp]
                        theorem LO.Arith.lh_mem_seqCons_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {x : V} {z : V} (H : LO.Arith.Seq s) :
                        LO.Arith.lh s, x s ⁀' z x = z
                        theorem LO.Arith.Seq.mem_seqCons_iff_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {s : V} {x : V} {z : V} (hi : i < LO.Arith.lh s) :
                        i, x s ⁀' z i, x s
                        @[simp]
                        theorem LO.Arith.lh_not_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (Ss : LO.Arith.Seq s) (x : V) :
                        LO.Arith.lh s, xs
                        theorem LO.Arith.seqCons_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (t : V) (x : V) (s : V) :
                        t = s ⁀' x l2 * s, l = LO.Arith.lh s p(2 * s + x + 1) ^ 2, p = l, x t = insert p s
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • =
                          Equations
                          • =
                          theorem LO.Arith.seqCons_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : ) (a : ) :
                          (s ⁀' a) = s ⁀' a
                          theorem LO.Arith.Seq.eq_of_eq_of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s₁ : V} {s₂ : V} (H₁ : LO.Arith.Seq s₁) (H₂ : LO.Arith.Seq s₂) (hl : LO.Arith.lh s₁ = LO.Arith.lh s₂) (h : s₁ s₂) :
                          s₁ = s₂
                          theorem LO.Arith.subset_pair {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {t : V} (h : ∀ (i x : V), i, x si, x t) :
                          s t
                          theorem LO.Arith.Seq.lh_ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s₁ : V} {s₂ : V} (H₁ : LO.Arith.Seq s₁) (H₂ : LO.Arith.Seq s₂) (h : LO.Arith.lh s₁ = LO.Arith.lh s₂) (H : ∀ (i x₁ x₂ : V), i, x₁ s₁i, x₂ s₂x₁ = x₂) :
                          s₁ = s₂
                          @[simp]
                          theorem LO.Arith.Seq.seqCons_ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a₁ : V} {a₂ : V} {s₁ : V} {s₂ : V} (H₁ : LO.Arith.Seq s₁) (H₂ : LO.Arith.Seq s₂) :
                          s₁ ⁀' a₁ = s₂ ⁀' a₂ a₁ = a₂ s₁ = s₂
                          theorem LO.Arith.ne_zero_iff_one_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} :
                          a 0 1 a

                          TODO: move to Lemmata.lean

                          theorem LO.Arith.Seq.cases_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} :
                          LO.Arith.Seq s s = ∃ (x : V) (s' : V), LO.Arith.Seq s' s = s' ⁀' x
                          theorem LO.Arith.Seq.cases {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} :
                          LO.Arith.Seq ss = ∃ (x : V) (s' : V), LO.Arith.Seq s' s = s' ⁀' x

                          Alias of the forward direction of LO.Arith.Seq.cases_iff.

                          theorem LO.Arith.seq_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hnil : P ) (hcons : ∀ (s x : V), LO.Arith.Seq sP sP (s ⁀' x)) {s : V} :
                          LO.Arith.Seq sP s

                          !⟦x, y, z, ...⟧ notation for Seq

                          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
                              @[simp]
                              theorem LO.Arith.singleton_seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
                              LO.Arith.Seq !⟦x
                              @[simp]
                              theorem LO.Arith.doubleton_seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                              LO.Arith.Seq !⟦x, y
                              @[simp]
                              theorem LO.Arith.mem_singleton_seq_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                              0, x !⟦y x = y
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                instance LO.Arith.mkSeq₁_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
                                𝚺₀-Function₁ fun (x : V) => !⟦x
                                Equations
                                • =
                                Equations
                                • =
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  instance LO.Arith.mkSeq₂_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
                                  𝚺₁-Function₂ fun (x y : V) => !⟦x, y
                                  Equations
                                  • =
                                  instance LO.Arith.mkSeq₂_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                  { Γ := Γ, rank := m + 1 }-Function₂ fun (x y : V) => !⟦x, y
                                  Equations
                                  • =
                                  theorem LO.Arith.sigmaOne_skolem_seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : VVProp} (hP : 𝚺₁-Relation R) {l : V} (H : x < l, ∃ (y : V), R x y) :
                                  ∃ (s : V), LO.Arith.Seq s LO.Arith.lh s = l ∀ (i x : V), i, x sR i x
                                  theorem LO.Arith.sigmaOne_skolem_seq! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : VVProp} (hP : 𝚺₁-Relation R) {l : V} (H : x < l, ∃! y : V, R x y) :
                                  ∃! s : V, LO.Arith.Seq s LO.Arith.lh s = l ∀ (i x : V), i, x sR i x
                                  def LO.Arith.vecToSeq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } :
                                  (Fin nV)V
                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem LO.Arith.vecToSeq_vecCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } (v : Fin nV) (a : V) :
                                    @[simp]
                                    @[simp]
                                    theorem LO.Arith.lh_vecToSeq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } (v : Fin nV) :
                                    theorem LO.Arith.mem_vectoSeq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } (v : Fin nV) (i : Fin n) :
                                    i, v i LO.Arith.vecToSeq v
                                    theorem LO.Arith.order_ball_induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : VVV} (hf : 𝚺₁-Function₂ f) {P : VVProp} (hP : 𝚺₁-Relation P) (ind : ∀ (x y : V), (x' < x, y'f x y, P x' y')P x y) (x : V) (y : V) :
                                    P x y
                                    theorem LO.Arith.order_ball_induction_sigma1' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : VV} (hf : 𝚺₁-Function₁ f) {P : VVProp} (hP : 𝚺₁-Relation P) (ind : ∀ (x y : V), (x' < x, y'f y, P x' y')P x y) (x : V) (y : V) :
                                    P x y
                                    theorem LO.Arith.order_ball_induction₂_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {fy : VVVV} {fz : VVVV} (hfy : 𝚺₁-Function₃ fy) (hfz : 𝚺₁-Function₃ fz) {P : VVVProp} (hP : 𝚺₁-Relation₃ P) (ind : ∀ (x y z : V), (x' < x, y'fy x y z, z'fz x y z, P x' y' z')P x y z) (x : V) (y : V) (z : V) :
                                    P x y z
                                    theorem LO.Arith.order_ball_induction₃_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {fy : VVVVV} {fz : VVVVV} {fw : VVVVV} (hfy : 𝚺₁-Function₄ fy) (hfz : 𝚺₁-Function₄ fz) (hfw : 𝚺₁-Function₄ fw) {P : VVVVProp} (hP : 𝚺₁-Relation₄ P) (ind : ∀ (x y z w : V), (x' < x, y'fy x y z w, z'fz x y z w, w'fw x y z w, P x' y' z' w')P x y z w) (x : V) (y : V) (z : V) (w : V) :
                                    P x y z w