Menu
▾
▴
#391 Prove finiteness with injection
Dominique Cansell requests a reasoner to prove finiteness with an injective function: when the goal is finite(S), the user should be able to input a function from S to a set T in the Proof command, which would generate two sub-goals: that f is injective and that T is finite.
A similar reasoner could be used to prove that card(S)≤card(T) by providing an injective function from S to T.
