Function lemma_bijective_cardinality Copy item path

pub proof fn lemma_bijective_cardinality<A, B>(
    f: FnSpec<(A,), B>,
    domain: Set<A>,
    codomain: Set<B>,
)

bijective_on(f, domain, codomain),

domain.finite(),

codomain.finite(),

domain.len() == codomain.len(),