Commit 08468235 authored by Dennis Müller's avatar Dennis Müller

removed old files

parent 74a0b452
namespace http://mathhub.info/MitM/smglom/FinSequences ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import seq http://cds.omdoc.org/urtheories❚
import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚
theory FinSequneces2 : base:?Logic =
include arith:?NaturalArithmetics ❙
include sig:?LFSigma ❙
below : ℕ ⟶ type ❘ = [n] Σ x : ℕ . ⊦ x < n ❙
finSeq : ℕ ⟶ type ⟶ type ❘= [n,t] below n ⟶ t❙
sequenceLength : {n : ℕ, A : type} finSeq n A ⟶ ℕ ❘= [n,A ,f] n ❘# seqLen 3 ❙
prop_nonemptyFiniteSequence : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n, A , f] 0 < n ❘# prop_disjointFiniteSequence 3 ❙
prop_disjointFiniteSequence : {n : ℕ, A : type} finSeq n A ⟶ bool
❘= [n , A , f] ∀ [m1 : below n] ∀ [m2 : below n] ((πl m1) ≠ (πl m2)) ⇒ (f m1 ≠ f m2)
❘# prop_disjointFiniteSequence 3 ❙
representativeFiniteSeqeuence : {n : ℕ , A : type} finSeq n A ⟶ (A ⟶ ℕ) ⟶ ℕ ❙
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment