namespace  http://mathhub.info/MitM/core/typedsets ❚

import base http://mathhub.info/MitM/Foundation ❚
import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚


theory FiniteSets : base:?Logic =
	include ☞base:?ProductTypes ❙
	include ?AllSets ❙
	

	finiteSet : type ⟶ type ❘ = [t] Σ  x : (set t) . ⊦ x finite ❘# finSet 1 ❙
	
	setToFiniteSet : {A : type , s : set A} ⊦ s finite ⟶ finSet A ❘= [A,s,p] ⟨ s , p ⟩❙
	
	theorem_emptySetIsFinite : {A : type} ⊦ (∅ : set A) finite❙
	
	theorem_setConsFinite : {A : type, s : set A , a : A} ⊦ s finite ⟶ ⊦ (s <- a) finite❙ 
	
	theorem_setConsFiniteSplit : {A : type, s : set A , a : A } ⊦ (s <- a) finite ⟶ ⊦ s finite ❘ # setSpFin 2 3 4❙ // error , wenn keine notation dann fehle rin setsum -> bla ❙
❚