Theory: equipollence (cardinality)

Definition: equipollent
A ~ B ==  ∃f:A ⟶ B. Bij(A;B;f)

Lemma: equipollent_wf
∀[A,B:Type].  (A ~ B ∈ Type)

Lemma: equipollent-iff-inverse-funs
∀[A,B:Type].  (A ~ B ⇐⇒ ∃p:A ⟶ B × (B ⟶ A) [InvFuns(A;B;fst(p);snd(p))])

Lemma: equipollent-cardinality-le
∀[A:Type]. ∀[k:ℕ].  (A ~ ℕk ⇒ |A| ≤ k)

Lemma: cardinality-le_functionality_wrt_equipollence
∀[A,B:Type]. ∀[k:ℕ].  (A ~ B ⇒ {|A| ≤ k ⇐⇒ |B| ≤ k})

Lemma: one_one_corr_equipollent
∀[A,B:Type].  (1-1-Corresp(A;B) ⇐⇒ A ~ B)

Lemma: equipollent-decidable-equal
∀[A,B:Type].  (A ~ B ⇒ (∀x,y:B.  Dec(x = y ∈ B)) ⇒ {∀x,y:A.  Dec(x = y ∈ A)})

Lemma: equipollent_weakening
∀[A,B:Type].  A ~ B supposing A = B ∈ Type

Lemma: equipollent_inversion
∀[A,B:Type].  (A ~ B ⇒ B ~ A)

Lemma: equipollent_transitivity
∀[A,B,C:Type].  (A ~ B ⇒ B ~ C ⇒ A ~ C)

Lemma: equipollent-implies-equal
∀[k,m:ℕ].  k = m ∈ ℤ supposing ℕk ~ ℕm

Lemma: equipollent_same
∀[A:Type]. A ~ A

Lemma: product_functionality_wrt_equipollent_left
∀[A,B,C,D:Type].  (A ~ B ⇒ A × C ~ B × D supposing C = D ∈ Type)

Lemma: product_functionality_wrt_equipollent_right
∀[A,B,C:Type].  (A ~ B ⇒ C × A ~ C × B)

Lemma: product_functionality_wrt_equipollent
∀[A,B,C,D:Type].  (A ~ B ⇒ C ~ D ⇒ A × C ~ B × D)

Lemma: product_functionality_wrt_equipollent_dependent
∀[A,B:Type]. ∀[C:A ⟶ Type]. ∀[D:B ⟶ Type].
  ∀f:A ⟶ B. (Bij(A;B;f) ⇒ (∀a:A. C[a] ~ D[f a]) ⇒ a:A × C[a] ~ b:B × D[b])

Lemma: isect_functionality_wrt_equipollent_dependent
∀[A,B:Type]. ∀[C:A ⟶ Type]. ∀[D:B ⟶ Type].
  ∀f:A ⟶ B. (A ⇒ Bij(A;B;f) ⇒ (∀[a:A]. C[a] ~ D[f a]) ⇒ ⋂a:A. C[a] ~ ⋂b:B. D[b])

Lemma: equipollent_weakening_ext-eq
∀[A,B:Type].  A ~ B supposing A ≡ B

Lemma: equipollent_functionality_wrt_equipollent
∀[A1,A2,B1,B2:Type].  (A1 ~ A2 ⇒ B1 ~ B2 ⇒ (A1 ~ B1 ⇐⇒ A2 ~ B2))

Lemma: equipollent_functionality_wrt_ext-eq
∀[A1,A2,B1,B2:Type].  (A1 ~ B1 ⇐⇒ A2 ~ B2) supposing (B1 ≡ B2 and A1 ≡ A2)

Lemma: equipollent_functionality_wrt_ext-eq-right
∀[A,B1,B2:Type].  A ~ B1 ⇐⇒ A ~ B2 supposing B1 ≡ B2

Lemma: equipollent_functionality_wrt_ext-eq-left
∀[A1,A2,B1,B2:Type].  (A1 ~ B1 ⇐⇒ A2 ~ B2) supposing ((B1 = B2 ∈ Type) and A1 ≡ A2)

Lemma: equipollent_functionality_wrt_equipollent2
∀[A,B1,B2:Type].  (B1 ~ B2 ⇒ (A ~ B1 ⇐⇒ A ~ B2))

Lemma: equipollent_functionality_wrt_equipollent3
∀[A,B1,B2:Type].  (B2 ~ B1 ⇒ (B1 ~ A ⇐⇒ B2 ~ A))

Lemma: function_functionality_wrt_equipollent
∀[A:Type]. ∀[B,C:A ⟶ Type].  ((∀a:A. B[a] ~ C[a]) ⇒ a:A ⟶ B[a] ~ a:A ⟶ C[a])

Lemma: function_functionality_wrt_equipollent_left
∀[A,B,C:Type].  (A ~ B ⇒ A ⟶ C ~ B ⟶ C)

Lemma: function_functionality_wrt_equipollent_right
∀[A,B,C:Type].  (A ~ B ⇒ C ⟶ A ~ C ⟶ B)

Lemma: indep-function_functionality_wrt_equipollent
∀[A,B,C,D:Type].  (A ~ B ⇒ C ~ D ⇒ C ⟶ A ~ D ⟶ B)

Lemma: union_functionality_wrt_equipollent
∀[A,B,C,D:Type].  (A ~ B ⇒ C ~ D ⇒ A + C ~ B + D)

Lemma: equipollent-product-assoc
∀[A,B,C:Type].  A × B × C ~ A × B × C

Lemma: equipollent-product-com
∀[A,B:Type].  A × B ~ B × A

Lemma: equipollent-union-com
∀[A,B:Type].  A + B ~ B + A

Lemma: equipollent-function-product
∀[A,B,C:Type].  C ⟶ (A × B) ~ C ⟶ A × (C ⟶ B)

Lemma: equipollent-function-function
∀[A,B,C:Type].  A ⟶ B ⟶ C ~ (A × B) ⟶ C

Lemma: equipollent-union-function
∀[A,B,C:Type].  (A + B) ⟶ C ~ A ⟶ C × (B ⟶ C)

Lemma: equipollent-union-product
∀[A,B,C:Type].  A + B × C ~ A × C + (B × C)

Lemma: equipollent-identity
∀[A,B:Type].  (B ~ Unit ⇒ B × A ~ A)

Lemma: equipollent-unit
∀[T:Type]. (T ⇒ T ~ Unit supposing ∀x,y:T.  (x = y ∈ T))

Lemma: top-equipollent-unit
Top ~ Unit

Lemma: equipollent-identity-left
∀[A:Type]. Top × A ~ A

Lemma: equipollent-identity-right
∀[A:Type]. A × Top ~ A

Lemma: equipollent-product-one
∀[A:Type]. (A × ℕ1 ~ A ∧ ℕ1 × A ~ A)

Lemma: equipollent-product-zero
∀[A:Type]. (A × ℕ0 ~ ℕ0 ∧ ℕ0 × A ~ ℕ0)

Lemma: equipollent-sum-zero
∀[A:Type]. (A + ℕ0 ~ A ∧ ℕ0 + A ~ A)

Lemma: equipollent-nsub
∀n,m:ℕ.  (n = m ∈ ℤ ⇐⇒ ℕn ~ ℕm)

Lemma: equipollent_interval
∀a,b:ℤ.  {a..b^-} ~ ℕb - a

Lemma: equipollent-multiply
∀a,b:ℕ.  ℕa × ℕb ~ ℕa * b

Lemma: equipollent-add
∀a,b:ℕ.  ℕa + ℕb ~ ℕa + b

Lemma: equipollent-iff-list
∀[T:Type]. ∀n:ℕ. (T ~ ℕn ⇐⇒ ∃L:T List. (no_repeats(T;L) ∧ (||L|| = n ∈ ℤ) ∧ (∀x:T. (x ∈ L))))

Lemma: equipollent-set
∀[T:Type]. ∀[P:T ⟶ ℙ].  {x:T| P[x]}  ~ {x:T| ↓P[x]}

Lemma: equipollent-sets
∀[T:Type]. ∀[P,Q:T ⟶ ℙ].  {x:T| P[x]}  ~ {x:T| Q[x]}  supposing ∀x:T. (P[x] ⇐⇒ Q[x])

Lemma: equipollent-split
∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Dec(↓P[x])) ⇒ T ~ {x:T| P[x]}  + {x:T| ¬P[x]} )

Lemma: equipollent-zero
∀[A:Type]. (A ~ ℕ0 ⇐⇒ ¬A)

Lemma: equipollent-non-zero
∀[T:Type]. ∀n:ℕ⁺. (T ~ ℕn ⇒ T)

Lemma: equipollent-one-iff
∀[A:Type]. (A ~ ℕ1 ⇐⇒ ∃z:A. ∀x:A. (x = z ∈ A))

Lemma: equipollent-one
∀[A:Type]. ∀a:A. {x:A| x = a ∈ A}  ~ ℕ1

Lemma: equipollent-two
𝔹 ~ ℕ2

Lemma: equipollent-int_seg
∀n,m:ℤ.  {n..m^-} ~ ℕif n <z m then m - n else 0 fi

Lemma: equipollent-int_seg-shift
∀n:ℤ. ∀m:ℕ.  {n..n + m^-} ~ ℕm

Definition: singleton-type
singleton-type(A) ==  ∃a:A. ∀a':A. (a' = a ∈ A)

Lemma: singleton-type_wf
∀[A:Type]. (singleton-type(A) ∈ Type)

Lemma: singleton-type-top
singleton-type(Top)

Lemma: singleton-type-void-domain
∀[A:Type]. ∀[B:A ⟶ Type].  singleton-type(a:A ⟶ B[a]) supposing ¬A

Lemma: singleton-type-product
∀[A,B:Type].  (singleton-type(A) ⇒ singleton-type(B) ⇒ singleton-type(A × B))

Lemma: singleton-type-function
∀[A:Type]. ∀[B:A ⟶ Type].  ((∀a:A. singleton-type(B[a])) ⇒ singleton-type(a:A ⟶ B[a]))

Lemma: singleton-type-one
singleton-type(ℕ1)

Definition: powerset
powerset(T) ==  T ⟶ ℕ2

Lemma: powerset_wf
∀[T:Type]. (powerset(T) ∈ Type)

Lemma: equipollent-singletons
∀[A,B:Type].  (singleton-type(A) ⇒ singleton-type(B) ⇒ A ~ B)

Lemma: equipollent-void-domain
∀[A:Type]. ℕ0 ⟶ A ~ ℕ1

Lemma: equipollent-empty-domain
∀[S:Type]. ((¬S) ⇒ (∀[A:S ⟶ Type]. u:S ⟶ (A u) ~ ℕ1))

Lemma: equipollent-singleton-domain
∀[S:Type]. ∀s:singleton-type(S). ∀[A:S ⟶ Type]. u:S ⟶ (A u) ~ A (fst(s))

Lemma: equipollent-singleton-domain2
∀[S:Type]. (singleton-type(S) ⇒ (∀[A:Type]. S ⟶ A ~ A))

Lemma: equipollent-exp
∀n,b:ℕ.  ℕn ⟶ ℕb ~ ℕb^n

Lemma: equipollent-powerset
∀n:ℕ. ∀T:Type.  (T ~ ℕn ⇒ powerset(T) ~ ℕ2^n)

Lemma: equipollent-sum
∀n:ℕ. ∀f:ℕn ⟶ ℕ.  i:ℕn × ℕf[i] ~ ℕΣ(f[i] | i < n)

Lemma: equipollent-product
∀n:ℕ. ∀f:ℕn ⟶ ℕ.  i:ℕn ⟶ ℕf[i] ~ ℕΠ(f[i] | i < n)

Lemma: equipollent-quotient

∀[A:Type]. ∀E:A ⟶ A ⟶ 𝔹. A ~ a:x,y:A//(↑E[x;y]) × {b:A| ↑E[a;b]}  supposing EquivRel(A;x,y.↑E[x;y])

Lemma: equipollent-quotient2
∀[A:Type]
∀E:A ⟶ A ⟶ ℙ. ∀d:∀x,y:A. Dec(↓E[x;y]).
A ~ a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} supposing EquivRel(A;x,y.↓E[x;y])

Definition: equiv-equipollent

A ~ B mod (a1,a2.E[a1; a2]) ==  ∃f:A ⟶ B. (Surj(A;B;f) ∧ (∀a1,a2:A.  ((f a1) = (f a2) ∈ B

⇐⇒ ↓E[a1; a2])))

Lemma: equiv-equipollent_wf
∀[A,B:Type]. ∀[E:A ⟶ A ⟶ ℙ].  (A ~ B mod (a1,a2.E[a1;a2]) ∈ ℙ)

Lemma: equiv-equipollent-implies-quotient-equipollent
∀[A,B:Type].  ∀E:A ⟶ A ⟶ ℙ. A ~ B mod (a1,a2.E[a1;a2]) ⇒ x,y:A//E[x;y] ~ B supposing EquivRel(A;x,y.E[x;y])

Lemma: equiv-equipollent-iff-quotient-equipollent
∀[A,B:Type].
  ∀E:A ⟶ A ⟶ ℙ
    ((∃g:(x,y:A//E[x;y]) ⟶ A. ∀c:x,y:A//E[x;y]. ((g c) = c ∈ (x,y:A//E[x;y])))
    ∨ (∀f:A ⟶ B. ∀b:B.  SqStable(∃a:A. ((f a) = b ∈ B))))
    ⇒ (A ~ B mod (a1,a2.E[a1;a2]) ⇐⇒ x,y:A//E[x;y] ~ B)
    supposing EquivRel(A;x,y.E[x;y])

Lemma: quotient-equipollent
∀[A,B:Type].
  (finite-type(A)
  ⇒ (∀x,y:B.  Dec(x = y ∈ B))
  ⇒ (∀E:A ⟶ A ⟶ ℙ. x,y:A//E[x;y] ~ B ⇐⇒ A ~ B mod (a1,a2.E[a1;a2]) supposing EquivRel(A;x,y.E[x;y])))

Lemma: quotient-equipollent-nat
∀[A:Type]. ∀[k:ℕ].
  (finite-type(A)
  ⇒ (∀E:A ⟶ A ⟶ ℙ. x,y:A//E[x;y] ~ ℕk ⇐⇒ A ~ ℕk mod (a1,a2.E[a1;a2]) supposing EquivRel(A;x,y.E[x;y])))

Lemma: equipollent-partition
∀k:ℕ
  ∀[A:Type]
    (A ~ ℕk
    ⇒ (∀[P:A ⟶ ℙ]. ((∀x:A. Dec(P[x])) ⇒ (∃i,j:ℕ. ((k = (i + j) ∈ ℤ) ∧ {a:A| P[a]}  ~ ℕi ∧ {a:A| ¬P[a]}  ~ ℕj)))))

Lemma: equipollent-subtract
∀a,b:ℕ.  ∀[P:ℕa ⟶ ℙ]. ({x:ℕa| P[x]}  ~ ℕb ⇒ {x:ℕa| ¬P[x]}  ~ ℕa - b)

Lemma: equipollent-subtract2
∀a,b:ℕ.  ∀[T:Type]. (T ~ ℕa ⇒ (∀[P:T ⟶ ℙ]. ({x:T| P[x]}  ~ ℕb ⇒ {x:T| ¬P[x]}  ~ ℕa - b)))

Lemma: equipollent-subtract-one
∀a:ℕ. ∀i:ℕa.  {x:ℕa| ¬(x = i ∈ ℕa)}  ~ ℕa - 1

Lemma: equipollent-general-subtract-one
∀a:ℕ. ∀[T:Type]. (T ~ ℕa ⇒ (∀i:T. {x:T| ¬(x = i ∈ T)}  ~ ℕa - 1))

Lemma: equipollent-length
∀[T:Type]. ∀L:T List. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ {x:T| (x ∈ L)}  ~ ℕ||L|| supposing no_repeats(T;L))

Lemma: equipollent-list
∀[T:Type]. ∀k:ℕ. (T ~ ℕk ⇒ (∀n:ℕ. {as:T List| ||as|| = n ∈ ℤ}  ~ ℕk^n))

Lemma: equipollent-int-nat
ℤ ~ ℕ

Lemma: decidable__equal_equipollent
∀[T:Type]. ∀k:ℕ. (T ~ ℕk ⇒ (∀a,b:T.  Dec(a = b ∈ T)))

Lemma: equipollent-subtype
∀[T,A:Type].
  (∀[a,b:ℕ].  (a ≤ b) supposing (T ~ ℕb and A ~ ℕa)) supposing
     ((∀a1,a2:A.  ((a1 = a2 ∈ T) ⇒ (a1 = a2 ∈ A))) and
     (A ⊆r T))

Lemma: equipollent-product-sum

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:a:A ⟶ B[a] ⟶ Type].  x:A ⟶ (y:B[x] × C[x;y]) ~ f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x])

Lemma: equipollent-product-product

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:a:A ⟶ B[a] ⟶ Type].  x:A ⟶ y:B[x] ⟶ C[x;y] ~ p:(a:A × B[a]) ⟶ C[fst(p);snd(p)]

Lemma: equipollent-union-sum
∀[A,B:Type]. ∀[C:A ⟶ Type]. ∀[D:B ⟶ Type].
  a:A × C[a] + (b:B × D[b]) ~ d:A + B × case d of inl(a) => C[a] | inr(b) => D[b]

Lemma: distinct-representatives
∀k:ℕ
  ∀[A:Type]
    (A ~ ℕk
    ⇒ (∀[E:A ⟶ A ⟶ ℙ]
          (EquivRel(A;x,y.E[x;y])
          ⇒ (∀x,y:A.  Dec(E[x;y]))
          ⇒ (∃L:A List. ((∀a,b∈L.  ¬E[a;b]) ∧ (∀a:A. (∃b∈L. E[a;b])) ∧ (||L|| ≤ k))))))

Lemma: equipollent-distinct-representatives
∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
  (EquivRel(A;x,y.E[x;y]) ⇒ (∀L:A List. (∀a:A. (∃b∈L. E[a;b])) ⇒ x,y:A//E[x;y] ~ ℕ||L|| supposing (∀a,b∈L.  ¬E[a;b])))

Lemma: count-by-equiv
∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
  (EquivRel(A;x,y.E[x;y])
  ⇒ (∀L:A List. (∀a:A. (∃b∈L. E[a;b])) ⇒ A ~ i:ℕ||L|| × {a:A| E[a;L[i]]}  supposing (∀a,b∈L.  ¬E[a;b])))

Lemma: count-by-decidable-equiv
∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
  (EquivRel(A;x,y.E[x;y])
  ⇒ (∀x,y:A.  Dec(E[x;y]))
  ⇒ (∀k:ℕ
        (A ~ ℕk
        ⇒ (∃L:A List
             ((∀a,b∈L.  ¬E[a;b])
             ∧ (∀a:A. (∃b∈L. E[a;b]))

             ∧ (∃f:ℕ||L|| ⟶ ℕ. ((∀i:ℕ||L||. {a:A| E[a;L[i]]}  ~ ℕf i) ∧ A ~ i:ℕ||L|| × ℕf i ∧ (k = Σ(f i | i < ||L||) ∈\000C ℤ))))))))

Lemma: count-quotient
∀k:ℕ
  ∀[A:Type]
    (A ~ ℕk
    ⇒ (∀[E:A ⟶ A ⟶ ℙ]. (EquivRel(A;x,y.E[x;y]) ⇒ (∀x,y:A.  Dec(E[x;y])) ⇒ (∃j:ℕ. ((j ≤ k) ∧ x,y:A//E[x;y] ~ ℕj)))))

Lemma: count-by-orbits
∀n:ℕ
  ∀[T:Type]
    (T ~ ℕn
    ⇒ (∀f:T ⟶ T
          ∃orbits:T List List
           ((∀o∈orbits.orbit(T;f;o))
           ∧ (∀a:T. (∃o∈orbits. (a ∈ o)))
           ∧ (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
           ∧ no_repeats(T List;orbits)
           ∧ (n = l_sum(map(λo.||o||;orbits)) ∈ ℤ))
          supposing Inj(T;T;f)))

Lemma: involution-has-fixpoint
∀n:ℕ
  ∀[T:Type]. (T ~ ℕn ⇒ (∀f:T ⟶ T. ((∀x:T. ((f (f x)) = x ∈ T)) ⇒ ((n rem 2) = 1 ∈ ℤ) ⇒ (∃x:T. ((f x) = x ∈ T)))))

Lemma: involution-with-unique-fixpoint
∀n:ℕ
  ∀[T:Type]
    (T ~ ℕn
    ⇒ (∀f:T ⟶ T
          ((∀x:T. ((f (f x)) = x ∈ T))
          ⇒ (∀x,y:T.  (((f x) = x ∈ T) ⇒ ((f y) = y ∈ T) ⇒ (x = y ∈ T)))
          ⇒ ((n rem 2) = 1 ∈ ℤ ⇐⇒ ∃x:T. ((f x) = x ∈ T)))))

Definition: finite'
finite'(T) ==  ∀f:T ⟶ T. (Inj(T;T;f) ⇒ Surj(T;T;f))

Lemma: finite'_wf
∀[T:Type]. (finite'(T) ∈ ℙ)

Lemma: nsub_finite'
∀n:ℕ. finite'(ℕn)

Lemma: finite'_functionality_wrt_equipollent
∀[A,B:Type].  (A ~ B ⇒ (finite'(A) ⇐⇒ finite'(B)))

Definition: finite
finite(T) ==  ∃n:ℕ. T ~ ℕn

Lemma: finite_wf
∀[T:Type]. (finite(T) ∈ ℙ)

Lemma: finite-decidable-inhabited
∀[T:Type]. (finite(T) ⇒ (T ∨ (¬T)))

Lemma: decidable__equal_finite
Finite types have decidable equality.
We have to put a `guard` on the conclusion because otherwise the
tactic ProveDecidable will try to use this lemma to prove, for example,
that ⌜ℤ⌝ has decidable equality -- but ⌜ℤ⌝ is not finite, so the tactic fails.⋅

∀T:Type. (finite(T) ⇒ {∀x,y:T.  Dec(x = y ∈ T)})

Lemma: decidable-exists-finite
∀[T:Type]. (finite(T) ⇒ (∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∃t:T. P[t]))))

Lemma: decidable-all-finite
∀[T:Type]. (finite(T) ⇒ (∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∀t:T. P[t]))))

Lemma: finite-iff-listable
∀[T:Type]. (finite(T) ⇐⇒ ∃L:T List. (no_repeats(T;L) ∧ (∀x:T. (x ∈ L))))

Lemma: nsub_finite
∀n:ℕ. finite(ℕn)

Lemma: int_seg_finite
∀n,m:ℤ.  finite({n..m^-})

Lemma: finite_functionality_wrt_equipollent
∀[A,B:Type].  (A ~ B ⇒ (finite(A) ⇐⇒ finite(B)))

Lemma: finite_functionality_wrt_ext-eq
∀[A,B:Type].  (A ≡ B ⇒ (finite(A) ⇐⇒ finite(B)))

Lemma: finite-implies-finite'
∀[A:Type]. (finite(A) ⇒ finite'(A))

Lemma: finite-function
∀S:Type. ∀T:S ⟶ Type.  (finite(S) ⇒ (∀s:S. finite(T[s])) ⇒ finite(s:S ⟶ T[s]))

Lemma: finite-indep-fun
∀S,T:Type.  (finite(S) ⇒ finite(T) ⇒ finite(S ⟶ T))

Lemma: finite-product
∀[S:Type]. ∀[T:S ⟶ Type].  (finite(S) ⇒ (∀s:S. finite(T[s])) ⇒ finite(s:S × T[s]))

Lemma: finite-union
∀S,T:Type.  (finite(S) ∧ finite(T) ⇐⇒ finite(S + T))

Lemma: finite-unit
finite(Unit)

Lemma: finite-bool
finite(𝔹)

Lemma: finite-decidable-subset
∀T:Type. ∀B:T ⟶ ℙ.  (finite(T) ⇒ (∀x:T. Dec(↓B[x])) ⇒ finite({t:T| B[t]} ))

Lemma: finite-quotient
∀A:Type. ∀R:A ⟶ A ⟶ ℙ.  (finite(A) ⇒ EquivRel(A;x,y.x R y) ⇒ (∀x,y:A.  Dec(x R y)) ⇒ finite(x,y:A//(x R y)))

Lemma: finite-quotient-bound
∀A:Type. ∀R:A ⟶ A ⟶ ℙ. ∀n:ℕ.
  (A ~ ℕn ⇒ EquivRel(A;x,y.x R y) ⇒ (∀x,y:A.  Dec(x R y)) ⇒ (∃m:ℕ. ((m ≤ n) ∧ x,y:A//(x R y) ~ ℕm)))

Lemma: finite-injective-quotient
∀T,S:Type. ∀f:T ⟶ S.  (finite(S) ⇒ (∀s:S. Dec(∃t:T. (f[t] = s ∈ S))) ⇒ finite(T//t.f[t]))

Lemma: finite-fixed-length
∀T:Type. ∀n:ℕ.  (finite(T) ⇒ finite({l:T List| ||l|| = n ∈ ℤ} ))

Lemma: finite-type-equipollent
∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (finite-type(T) ⇐⇒ ∃n:ℕ. ℕn ~ T))

Lemma: finite-type-implies-finite
∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ finite-type(T) ⇒ finite(T))

Lemma: finite-function-equipollent
∀n:ℕ⁺. ∀[F:ℕn ⟶ Type]. i:ℕn ⟶ F[i] ~ i:ℕn - 1 ⟶ F[i] × F[n - 1]

Lemma: not-not-finite-xmiddle-1
∀[T:Type]. ((∃n:ℕ. ∃f:ℕn ⟶ T. Surj(ℕn;T;f)) ⇒ (∀P:T ⟶ ℙ. (¬¬(∀i:T. (P[i] ∨ (¬P[i]))))))

Lemma: not-not-finite-xmiddle
∀[T:Type]. (finite(T) ⇒ (∀P:T ⟶ ℙ. (¬¬(∀i:T. (P[i] ∨ (¬P[i]))))))

Lemma: not-not-finite-exists-or-all
∀[T:Type]. (finite(T) ⇒ (∀P:T ⟶ ℙ. (¬¬((∃i:T. P[i]) ∨ (∀i:T. (¬P[i]))))))

Lemma: not-not-finite-all-or-exists
∀[T:Type]. (finite(T) ⇒ (∀P:T ⟶ ℙ. (¬¬((∀i:T. P[i]) ∨ (∃i:T. (¬P[i]))))))

Lemma: void-function-equipollent
∀F:Top. i:ℕ0 ⟶ F[i] ~ Top

Lemma: equipollent-filter
∀[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List.  {x:ℕ||L||| ↑P[L[x]]}  ~ ℕ||filter(P;L)||

Lemma: tuple-type-append-equipollent
∀L1,L2:Type List.  tuple-type(L1) × tuple-type(L2) ~ tuple-type(L1 @ L2)

Lemma: tuple-type-concat

∀[T:Type]. ∀f:T ⟶ (Type List). ∀L:T List.  tuple-type(map(λi.tuple-type(f i);L)) ~ tuple-type(concat(map(f;L)))

Lemma: finite-acyclic-rel
∀[T:Type]. ((∃n:ℕ. T ~ ℕn) ⇒ (∀[R:T ⟶ T ⟶ ℙ]. ((∀x,y:T.  Dec(x R y)) ⇒ (SWellFounded(x R y) ⇐⇒ acyclic-rel(T;R)))))

Lemma: decidable__all_finite
∀[T:Type]. ∀k:ℕ. (T ~ ℕk ⇒ (∀[P:T ⟶ ℙ]. ((∀x:T. Dec(P[x])) ⇒ Dec(∀x:T. P[x]))))

Lemma: decidable__all_fun
∀[A,B:Type]. ∀[P:(A ⟶ B) ⟶ ℙ].  ((∃a:ℕ. A ~ ℕa) ⇒ (∃b:ℕ. B ~ ℕb) ⇒ (∀f:A ⟶ B. Dec(P[f])) ⇒ Dec(∀f:A ⟶ B. P[f]))

Lemma: decidable__all_length
∀[T:Type]. ∀[P:(T List) ⟶ ℙ].
  ((∀L:T List. Dec(P[L])) ⇒ (∃k:ℕ. T ~ ℕk) ⇒ (∀n:ℕ. Dec(∀L:T List. ((||L|| = n ∈ ℤ) ⇒ P[L]))))

Lemma: not-all-finite
∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Dec(P[x])) ⇒ (∃k:ℕ. T ~ ℕk) ⇒ (¬(∀x:T. P[x]) ⇐⇒ ∃x:T. (¬P[x])))

Lemma: decidable__all_length_bool
∀[P:(𝔹 List) ⟶ ℙ]. ((∀L:𝔹 List. Dec(P[L])) ⇒ (∀n:ℕ. Dec(∀L:𝔹 List. ((||L|| = n ∈ ℤ) ⇒ P[L]))))

Lemma: decidable__exists_length
∀[T:Type]. ∀[P:(T List) ⟶ ℙ].
  ((∀L:T List. Dec(P[L])) ⇒ (∃k:ℕ. T ~ ℕk) ⇒ (∀n:ℕ. Dec(∃L:T List. ((||L|| = n ∈ ℤ) ∧ P[L]))))

Lemma: decidable__exists_length_bool
∀[P:(𝔹 List) ⟶ ℙ]. ((∀L:𝔹 List. Dec(P[L])) ⇒ (∀n:ℕ. Dec(∃L:𝔹 List. ((||L|| = n ∈ ℤ) ∧ P[L]))))

Lemma: length-filter-lower-bound

∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List]. ∀[T:Type]. ∀[k:ℕ]. ∀[f:{i:ℕ||L||| ¬↑P[L[i]]}  ⟶ T].

((||L|| - k) ≤ ||filter(P;L)||) supposing (T ~ ℕk and Inj({i:ℕ||L||| ¬↑P[L[i]]} ;T;f))

Lemma: n-to-bool-list
∀n:ℕ. ∃L:(ℕn ⟶ 𝔹) List. (no_repeats(ℕn ⟶ 𝔹;L) ∧ (∀f:ℕn ⟶ 𝔹. (f ∈ L)))

Home Index