| Metric | Count |
|---|
| Definitions | 0 |
Theoremspreimage, of_image, of_preimage, preimage, range_comp, set_image, compl_image_eq, existsUnique_of_mem_range, image_injective, image_strictMono, mem_range_iff_existsUnique, mem_set_image, preimage_image, preimage_surjective, subsingleton_image_iff, image_eq_preimage_symm, preimage, image_eq, image_image, mem_preimage_iff, preimage_preimage, set_image, image_preimage, image_surjective, nonempty_preimage, preimage_injective, preimage_subset_preimage_iff, range_comp, range_eq, preimage, mem_range_succ, image_elim_range_some_eq_range, injective_iff, range_elim, range_eq, range_fst, range_snd, image_nontrivial_iff, image, image_const, of_image, preimage, preimage', subset_preimage_const, image, image_of_injOn, preimage, range_mk'', image, preimage, elim_range, canLift, coe_comp_rangeFactorization, compl_compl_image, compl_image, compl_image_set_of, compl_range_inl, compl_range_inr, compl_range_some, disjoint_image_iff, disjoint_image_image, disjoint_image_inl_image_inr, disjoint_image_inl_range_inr, disjoint_image_left, disjoint_image_of_injective, disjoint_image_right, disjoint_powerset_insert, disjoint_preimage_iff, disjoint_range_inl_image_inr, eq_preimage_iff_image_eq, eq_preimage_subtype_val_iff, exists_eq_const_of_preimage_singleton, exists_image_iff, exists_mem_image, exists_range_iff, exists_subset_image_iff, exists_subset_range_and_iff, exists_subtype_range_iff, forall_mem_image, forall_mem_range, forall_subset_image_iff, forall_subset_range_iff, forall_subtype_range_iff, imageFactorization_eq, imageFactorization_surjective, image_comm, image_comp, image_comp_eq, image_compl_eq, image_compl_eq_range_diff_image, image_compl_preimage, image_compl_subset, image_congr, image_congr', image_diff, image_diff_preimage, image_empty, image_eq_empty, image_eq_image, image_eq_preimage_of_inverse, image_eq_range, image_eta, image_id, image_id', image_id_eq, image_image, image_injective, image_insert_eq, image_inter, image_inter_nonempty_iff, image_inter_on, image_inter_preimage, image_inter_subset, image_iterate_eq, image_mono, image_nonempty, image_nontrivial, image_of_range_union_range_eq_univ, image_pair, image_perm, image_preimage_eq, image_preimage_eq_iff, image_preimage_eq_inter_range, image_preimage_eq_of_subset, image_preimage_eq_range_inter, image_preimage_inl_union_image_preimage_inr, image_preimage_inter, image_preimage_subset, image_singleton, image_subset_iff, image_subset_image_iff, image_subset_preimage_of_inverse, image_subset_range, image_sumElim, image_surjective, image_swap_eq_preimage_swap, image_symmDiff, image_union, image_union_image_compl_eq_range, image_univ, image_univ_of_surjective, insert_image_compl_eq_range, insert_none_range_some, instNonemptyElemImage, instNonemptyRange, inter_preimage_subset, isCompl_range_inl_range_inr, isCompl_range_some_none, leftInverse_rangeSplitting, mem_compl_image, mem_image_iff_of_inverse, mem_range_of_mem_image, monotone_image, nonempty_of_nonempty_preimage, nontrivial_of_image, nontrivial_of_preimage, powerset_insert, powerset_insert_injOn, preimage_comp, preimage_comp_eq, preimage_compl, preimage_compl_eq_image_compl, preimage_congr, preimage_const, preimage_const_of_mem, preimage_const_of_notMem, preimage_diff, preimage_empty, preimage_eq_empty, preimage_eq_empty_iff, preimage_eq_iff_eq_image, preimage_eq_preimage, preimage_eq_preimage', preimage_eq_univ_iff, preimage_id, preimage_id', preimage_id_eq, preimage_image_eq, preimage_image_preimage, preimage_image_univ, preimage_injective, preimage_inl_image_inr, preimage_inl_range_inr, preimage_inr_image_inl, preimage_inr_range_inl, preimage_inter, preimage_inter_range, preimage_ite, preimage_iterate_eq, preimage_mono, preimage_preimage, preimage_range, preimage_rangeSplitting, preimage_range_inter, preimage_setOf_eq, preimage_singleton_eq_empty, preimage_singleton_false, preimage_singleton_nonempty, preimage_singleton_true, preimage_subset, preimage_subset_iff, preimage_subset_image_of_inverse, preimage_subset_of_surjOn, preimage_subset_preimage_iff, preimage_subtype_coe_eq_compl, preimage_sumElim, preimage_surjective, preimage_symmDiff, preimage_union, preimage_univ, prod_quotient_preimage_eq_image, rangeFactorization_coe, rangeFactorization_eq, rangeSplitting_injective, range_comp, range_comp', range_comp_subset_range, range_const, range_const_subset, range_diff_image, range_diff_image_subset, range_eq_empty, range_eq_empty_iff, range_eq_iff, range_eq_singleton, range_eq_singleton_iff, range_eq_univ, range_eval, range_id, range_id', range_image, range_inclusion, range_inl, range_inl_inter_range_inr, range_inl_union_range_inr, range_inr, range_inr_inter_range_inl, range_inr_union_range_inl, range_insert, range_inter_ssubset_iff_preimage_ssubset, range_ite_subset, range_ite_subset', range_nonempty, range_nonempty_iff_nonempty, range_quot_lift, range_quot_mk, range_quotient_lift, range_quotient_lift_on', range_quotient_mk, range_quotient_mk', range_singleton, range_some_inter_none, range_some_union_none, range_subset_iff, range_subset_range_iff_exists_comp, range_subset_singleton, range_subtype_map, range_unique, rightInverse_rangeSplitting, subset_image_compl, subset_image_diff, subset_image_iff, subset_image_symmDiff, subset_image_union, subset_preimage_image, subset_preimage_univ, subset_range_iff_exists_image_eq, subset_range_of_surjective, subsingleton_of_image, subsingleton_of_preimage, subsingleton_range, surjective_onto_image, surjective_onto_range, union_preimage_subset, coe_image, coe_image_of_subset, coe_image_subset, coe_image_univ, coe_preimage_self, exists_set_subtype, forall_set_subtype, image_preimage_coe, image_preimage_val, preimage_coe_compl, preimage_coe_compl', preimage_coe_eq_empty, preimage_coe_eq_preimage_coe_iff, preimage_coe_inter_self, preimage_coe_nonempty, preimage_coe_self_inter, preimage_val_eq_preimage_val_iff, preimage_val_subset_preimage_val_iff, range_coe, range_coe_subtype, range_val, range_val_subtype, range_eq, sigma_mk_preimage_image', sigma_mk_preimage_image_eq_self | 299 |
| Total | 299 |