SchroederBernstein

Statistics

Metric	Count
Definitions	0
Theorems `antisymm`, `min_injective`, `schroeder_bernstein`, `schroeder_bernstein_of_rel`, `total`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm` 📖	mathematical	—	`Equiv`	—	`schroeder_bernstein`
`min_injective` 📖	—	—	—	—	`zorn_subset` `IsChain.total` `Set.instReflSubset` `Set.subset_sUnion_of_mem` `Classical.by_contradiction` `Classical.axiom_of_choice` `Maximal.prop` `Set.mem_insert` `Maximal.eq_of_subset` `Set.subset_insert` `Set.InjOn.injective` `Function.injective_surjInv`
`schroeder_bernstein` 📖	mathematical	—	`Function.Bijective`	—	`schroeder_bernstein_of_rel`
`schroeder_bernstein_of_rel` 📖	mathematical	—	`Function.Bijective`	—	`isEmpty_or_nonempty` `Function.isEmpty` `Equiv.bijective` `Set.compl_subset_compl_of_subset` `Set.image_mono` `OrderHom.map_lfp` `compl_injective` `compl_compl` `Function.leftInverse_invFun` `Function.LeftInverse.image_image` `Set.range_eq_univ` `Set.range_piecewise` `Set.union_compl_self` `Set.injective_piecewise_iff` `Function.Injective.injOn` `Set.mem_image` `Function.invFun_eq`
`total` 📖	mathematical	—	`Function.Embedding`	—	`min_injective`

---