Documentation

Arithmetization.ISigmaOne.HFS.Basic

Hereditary Finite Set Theory in $\mathsf{I} \Sigma_1$ #

@[simp]
theorem LO.Arith.susbset_insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (a : V) :
a insert x a
@[simp]
theorem LO.Arith.bitRemove_susbset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (a : V) :
theorem LO.Arith.lt_of_mem_dom {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {m : V} (h : x, y m) :
x < m
theorem LO.Arith.lt_of_mem_rng {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {m : V} (h : x, y m) :
y < m
theorem LO.Arith.insert_subset_insert_of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (x : V) (h : a b) :
insert x a insert x b
theorem LO.Arith.sUnion_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
∃! u : V, ∀ (x : V), x u ts, x t
def LO.Arith.sUnion {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
V
Equations
Instances For
    @[simp]
    theorem LO.Arith.mem_sUnion_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} :
    a ⋃ʰᶠ b cb, a c
    theorem LO.Arith.sUnion_lt_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (ha : 0 < a) :
    @[simp]
    theorem LO.Arith.sUnion_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
    theorem LO.Arith.sUnion_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {u : V} {s : V} :
    u = ⋃ʰᶠ s x < u + s, x u ts, x t
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • =
      def LO.Arith.union {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
      V
      Equations
      Instances For
        Equations
        • LO.Arith.instUnion_arithmetization = { union := LO.Arith.union }
        Instances For
          @[simp]
          theorem LO.Arith.mem_cup_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} {c : V} :
          a b c a b a c
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            instance LO.Arith.union_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
            𝚺₀-Function₂ fun (x x_1 : V) => x x_1
            Equations
            • =
            Equations
            • =
            theorem LO.Arith.insert_eq_union_singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (s : V) :
            insert a s = {a} s
            @[simp]
            theorem LO.Arith.union_polybound {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
            a b 2 * (a + b)
            Equations
            • =
            theorem LO.Arith.union_comm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
            a b = b a
            @[simp]
            theorem LO.Arith.union_succ_union_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
            a a b
            @[simp]
            theorem LO.Arith.union_succ_union_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
            b a b
            @[simp]
            theorem LO.Arith.union_succ_union_union_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) (c : V) :
            a a b c
            @[simp]
            theorem LO.Arith.union_succ_union_union_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) (c : V) :
            b a b c
            @[simp]
            @[simp]
            theorem LO.Arith.sInter_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
            ∃! u : V, ∀ (x : V), x u s ts, x t
            def LO.Arith.sInter {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
            V
            Equations
            Instances For
              theorem LO.Arith.mem_sInter_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {s : V} :
              x ⋂ʰᶠ s s ts, x t
              theorem LO.Arith.mem_sInter_iff_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {s : V} (h : s ) :
              x ⋂ʰᶠ s ts, x t
              def LO.Arith.inter {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
              V
              Equations
              Instances For
                Equations
                • LO.Arith.instInter_arithmetization = { inter := LO.Arith.inter }
                Instances For
                  @[simp]
                  theorem LO.Arith.mem_inter_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} {c : V} :
                  a b c a b a c
                  theorem LO.Arith.inter_comm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
                  a b = b a
                  theorem LO.Arith.inter_eq_self_of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : a b) :
                  a b = a
                  theorem LO.Arith.product_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
                  ∃! u : V, ∀ (x : V), x u ya, zb, x = y, z
                  def LO.Arith.product {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
                  V
                  Equations
                  Instances For
                    theorem LO.Arith.mem_product_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {a : V} {b : V} :
                    x a ×ʰᶠ b ya, zb, x = y, z
                    theorem LO.Arith.mem_product_iff' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {a : V} {b : V} :
                    @[simp]
                    theorem LO.Arith.pair_mem_product_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {a : V} {b : V} :
                    x, y a ×ʰᶠ b x a y b
                    theorem LO.Arith.pair_mem_product {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {a : V} {b : V} (hx : x a) (hy : y b) :
                    x, y a ×ʰᶠ b
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      instance LO.Arith.product_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
                      𝚺₀-Function₂ fun (x x_1 : V) => x ×ʰᶠ x_1
                      Equations
                      • =
                      Equations
                      • =
                      theorem LO.Arith.domain_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
                      ∃! d : V, ∀ (x : V), x d ∃ (y : V), x, y s
                      def LO.Arith.domain {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
                      V
                      Equations
                      Instances For
                        theorem LO.Arith.mem_domain_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {s : V} :
                        x LO.Arith.domain s ∃ (y : V), x, y s
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • =
                          Equations
                          • =
                          @[simp]
                          theorem LO.Arith.domain_singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                          LO.Arith.domain {x, y} = {x}
                          @[simp]
                          theorem LO.Arith.domain_insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) (s : V) :
                          @[simp]
                          theorem LO.Arith.mem_domain_of_pair_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {s : V} (h : x, y s) :

                          Range #

                          theorem LO.Arith.range_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
                          ∃! r : V, ∀ (y : V), y r ∃ (x : V), x, y s
                          def LO.Arith.range {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
                          V
                          Equations
                          Instances For
                            theorem LO.Arith.mem_range_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {y : V} {s : V} :
                            y LO.Arith.range s ∃ (x : V), x, y s
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • =
                              Equations
                              • =

                              Disjoint #

                              def LO.Arith.Disjoint {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (t : V) :
                              Equations
                              Instances For
                                theorem LO.Arith.Disjoint.iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {t : V} :
                                LO.Arith.Disjoint s t ∀ (x : V), xs xt
                                theorem LO.Arith.Disjoint.not_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {t : V} {x : V} (hs : x s) (ht : x t) :
                                @[simp]
                                theorem LO.Arith.Disjoint.singleton_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {a : V} :
                                LO.Arith.Disjoint {a} s as

                                Mapping #

                                Equations
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • =
                                    Equations
                                    • =
                                    theorem LO.Arith.IsMapping.get_exists_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} (h : LO.Arith.IsMapping m) {x : V} (hx : x LO.Arith.domain m) :
                                    ∃! y : V, x, y m
                                    def LO.Arith.IsMapping.get {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} (h : LO.Arith.IsMapping m) {x : V} (hx : x LO.Arith.domain m) :
                                    V
                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem LO.Arith.IsMapping.get_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} (h : LO.Arith.IsMapping m) {x : V} (hx : x LO.Arith.domain m) :
                                      x, h.get hx m
                                      theorem LO.Arith.IsMapping.get_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {y : V} {m : V} (h : LO.Arith.IsMapping m) {x : V} (hx : x LO.Arith.domain m) (hy : x, y m) :
                                      y = h.get hx
                                      theorem LO.Arith.IsMapping.union_of_disjoint_domain {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m₁ : V} {m₂ : V} (h₁ : LO.Arith.IsMapping m₁) (h₂ : LO.Arith.IsMapping m₂) (disjoint : LO.Arith.Disjoint (LO.Arith.domain m₁) (LO.Arith.domain m₂)) :
                                      @[simp]
                                      theorem LO.Arith.IsMapping.singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                      LO.Arith.IsMapping {x, y}
                                      theorem LO.Arith.IsMapping.insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {m : V} (h : LO.Arith.IsMapping m) (disjoint : xLO.Arith.domain m) :
                                      LO.Arith.IsMapping (insert x, y m)
                                      theorem LO.Arith.IsMapping.of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} {m' : V} (h : LO.Arith.IsMapping m) (ss : m' m) :
                                      theorem LO.Arith.IsMapping.uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} {x : V} {y₁ : V} {y₂ : V} (h : LO.Arith.IsMapping m) :
                                      x, y₁ mx, y₂ my₁ = y₂

                                      Restriction of mapping #

                                      theorem LO.Arith.restr_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) :
                                      ∃! g : V, ∀ (x : V), x g x f π₁ x s
                                      def LO.Arith.restr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) :
                                      V
                                      Equations
                                      Instances For
                                        theorem LO.Arith.mem_restr_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {f : V} {s : V} :
                                        @[simp]
                                        theorem LO.Arith.pair_mem_restr_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {f : V} {s : V} :
                                        x, y LO.Arith.restr f s x, y f x s
                                        @[simp]
                                        theorem LO.Arith.restr_subset_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) :
                                        @[simp]
                                        theorem LO.Arith.restr_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (f : V) (s : V) :
                                        theorem LO.Arith.insert_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hempty : P ) (hinsert : ∀ (a s : V), asP sP (insert a s)) (s : V) :
                                        P s
                                        theorem LO.Arith.insert_induction_sigmaOne {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚺₁-Predicate P) (hempty : P ) (hinsert : ∀ (a s : V), asP sP (insert a s)) (s : V) :
                                        P s
                                        theorem LO.Arith.insert_induction_piOne {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚷₁-Predicate P) (hempty : P ) (hinsert : ∀ (a s : V), asP sP (insert a s)) (s : V) :
                                        P s
                                        theorem LO.Arith.sigmaOne_skolem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : VVProp} (hP : 𝚺₁-Relation R) {s : V} (H : xs, ∃ (y : V), R x y) :
                                        ∃ (f : V), LO.Arith.IsMapping f LO.Arith.domain f = s ∀ (x y : V), x, y fR x y
                                        theorem LO.Arith.sigma₁_replacement {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : VV} (hf : 𝚺₁-Function₁ f) (s : V) :
                                        ∃! t : V, ∀ (y : V), y t xs, y = f x
                                        theorem LO.Arith.sigma₁_replacement₂ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : VVV} (hf : 𝚺₁-Function₂ f) (s₁ : V) (s₂ : V) :
                                        ∃! t : V, ∀ (y : V), y t x₁s₁, x₂s₂, y = f x₁ x₂
                                        def LO.Arith.fstIdx {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) :
                                        V
                                        Equations
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • =
                                            def LO.Arith.sndIdx {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) :
                                            V
                                            Equations
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • =