Subtype

Statistics

Metric	Count
Definitions `coind`, `instHasEquiv_mathlib`, `instSetoid_mathlib`, `map`, `restrict`	5
Theorems `extend_val_apply`, `extend_val_apply'`, `coe_eq_iff`, `coe_eq_of_eq_mk`, `coe_eta`, `coe_inj`, `coe_injective`, `coe_mk`, `coe_ne_coe`, `coe_prop`, `coind_coe`, `coind_injective`, `equiv_iff`, `equivalence`, `exists'`, `ext_iff_val`, `ext_val`, `forall'`, `heq_iff_coe_eq`, `heq_iff_coe_heq`, `map_coe`, `map_comp`, `map_def`, `map_eq`, `map_id`, `map_injective`, `map_involutive`, `map_ne`, `mk_eq_mk`, `prop`, `refl`, `restrict_apply`, `restrict_def`, `restrict_injective`, `surjective_restrict`, `trans`, `val_inj`, `val_injective`, `val_prop`, `exists_eq_subtype_mk_iff`, `exists_subtype_mk_eq_iff`	41
Total	46

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend_val_apply` 📖	mathematical	—	`extend`	—	`Injective.extend_apply` `Subtype.val_injective`
`extend_val_apply'` 📖	mathematical	—	`extend`	—	—

Subtype

Definitions

Name	Category	Theorems
`coind` 📖	CompOp	8 math math: `Continuous.subtype_coind`, `coind_injective`, `IsOpenMap.subtype_coind`, `coind_bijective`, `IsClosedMap.subtype_coind`, `coind_coe`, `coind_surjective`, `Set.Subtype.range_coind`
`instHasEquiv_mathlib` 📖	CompOp	3 math math: `equiv_iff`, `refl`, `equivalence`
`instSetoid_mathlib` 📖	CompOp	—
`map` 📖	CompOp	25 math math: `map_involutive`, `StarSubalgebra.inclusion_apply`, `List.filter_attach'`, `UniformContinuous.subtype_map`, `Unitary.map_coe`, `List.filter_attach`, `IsClosedMap.subtype_map`, `IsOpenMap.subtype_map`, `map_id`, `Multiset.filter_attach`, `cfcHomSuperset_apply`, `Set.range_subtype_map`, `SpectrumRestricts.starAlgHom_apply`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `map_eq`, `Measurable.subtype_map`, `map_injective`, `Equiv.coe_subtypeEquiv_eq_map`, `map_comp`, `Finset.filter_attach'`, `Continuous.subtype_map`, `cfcₙHomSuperset_apply`, `map_coe`, `Multiset.filter_attach'`, `map_def`
`restrict` 📖	CompOp	37 math math: `CategoryTheory.Limits.cokernelBiproductιIso_hom`, `restrict_apply`, `CategoryTheory.Limits.biproduct.fromSubtype_π_subtype`, `CategoryTheory.Limits.biproduct.fromSubtype_π_subtype_assoc`, `CategoryTheory.Limits.kernelForkBiproductToSubtype_cone`, `CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit`, `CategoryTheory.Limits.biproduct.fromSubtype_toSubtype_assoc`, `CategoryTheory.Limits.kernelBiproductπIso_hom`, `CategoryTheory.Limits.biproduct.toSubtype_π_assoc`, `CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom`, `CategoryTheory.Limits.instHasCokernelFromSubtype`, `CategoryTheory.Limits.biproduct.fromSubtype_π`, `CategoryTheory.Limits.biproduct.toSubtype_fromSubtype`, `surjective_restrict`, `restrict_injective`, `CategoryTheory.Limits.cokernelBiproductιIso_inv`, `CategoryTheory.Limits.kernelBiproductπIso_inv`, `CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_hom`, `CategoryTheory.Limits.biproduct.fromSubtype_π_assoc`, `CategoryTheory.Limits.biproduct.fromSubtype_eq_lift`, `Finset.univ_val_map_subtype_restrict`, `CategoryTheory.Limits.biproduct.ι_fromSubtype_assoc`, `CategoryTheory.Limits.biproduct.toSubtype_eq_desc`, `CategoryTheory.Limits.biproduct.ι_toSubtype_subtype_assoc`, `CategoryTheory.Limits.biproduct.fromSubtype_toSubtype`, `CategoryTheory.Limits.biproduct.ι_toSubtype`, `CategoryTheory.Limits.biproduct.ι_toSubtype_assoc`, `CategoryTheory.Limits.biproduct.toSubtype_fromSubtype_assoc`, `CategoryTheory.Limits.biproduct.ι_toSubtype_subtype`, `CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone`, `CategoryTheory.Limits.biproduct.toSubtype_π`, `CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv`, `CategoryTheory.Limits.instHasKernelToSubtype`, `CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit`, `CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv`, `restrict_def`, `CategoryTheory.Limits.biproduct.ι_fromSubtype`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_eq_iff` 📖	—	—	—	—	—
`coe_eq_of_eq_mk` 📖	—	—	—	—	—
`coe_eta` 📖	—	—	—	—	—
`coe_inj` 📖	—	—	—	—	`coe_injective`
`coe_injective` 📖	—	—	—	—	—
`coe_mk` 📖	—	—	—	—	—
`coe_ne_coe` 📖	—	—	—	—	`coe_injective`
`coe_prop` 📖	mathematical	—	`Set` `Set.instMembership`	—	`prop`
`coind_coe` 📖	mathematical	—	`coind`	—	—
`coind_injective` 📖	mathematical	—	`coind`	—	—
`equiv_iff` 📖	mathematical	—	`instHasEquiv_mathlib`	—	—
`equivalence` 📖	mathematical	—	`instHasEquiv_mathlib`	—	`refl` `symm` `trans`
`exists'` 📖	—	—	—	—	—
`ext_iff_val` 📖	—	—	—	—	—
`ext_val` 📖	—	—	—	—	—
`forall'` 📖	—	—	—	—	—
`heq_iff_coe_eq` 📖	—	—	—	—	—
`heq_iff_coe_heq` 📖	—	—	—	—	—
`map_coe` 📖	mathematical	—	`map`	—	—
`map_comp` 📖	mathematical	—	`map`	—	—
`map_def` 📖	mathematical	—	`map` `prop`	—	—
`map_eq` 📖	mathematical	—	`map`	—	—
`map_id` 📖	mathematical	—	`map`	—	—
`map_injective` 📖	mathematical	—	`map`	—	`coind_injective` `coe_injective`
`map_involutive` 📖	mathematical	`Function.Involutive`	`map`	—	—
`map_ne` 📖	—	—	—	—	`Iff.not` `map_eq`
`mk_eq_mk` 📖	—	—	—	—	—
`prop` 📖	—	—	—	—	—
`refl` 📖	mathematical	—	`instHasEquiv_mathlib`	—	—
`restrict_apply` 📖	mathematical	—	`restrict`	—	—
`restrict_def` 📖	mathematical	—	`restrict`	—	—
`restrict_injective` 📖	mathematical	—	`restrict`	—	`coe_injective`
`surjective_restrict` 📖	mathematical	—	`restrict`	—	—
`trans` 📖	—	`instHasEquiv_mathlib`	—	—	—
`val_inj` 📖	—	—	—	—	—
`val_injective` 📖	—	—	—	—	`coe_injective`
`val_prop` 📖	mathematical	—	`Set` `Set.instMembership`	—	`prop`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_subtype_mk_iff` 📖	—	—	—	—	`Subtype.coe_eq_iff`
`exists_subtype_mk_eq_iff` 📖	—	—	—	—	—

---

← Back to Index