Documentation Verification Report

OpenNhds

📁 Source: Mathlib/Topology/Category/TopCat/OpenNhds.lean

Statistics

Metric	Count
Definitions `adjunctionNhds`, `functorNhds`, `OpenNhds`, `inclusion`, `inclusionMapIso`, `infLELeft`, `infLERight`, `instInhabited`, `instLattice`, `instOrderTop`, `map`, `instFunLike`, `partialOrder`, `adjunctionNhds`, `functorNhds`	15
Theorems `functorNhds_map`, `functorNhds_obj_coe`, `apply_mk`, `coe_id`, `comp_apply`, `id_apply`, `inclusionMapIso_hom`, `inclusionMapIso_hom_app`, `inclusionMapIso_inv`, `inclusionMapIso_inv_app`, `inclusion_obj`, `isOpenEmbedding`, `map_id_obj`, `map_id_obj'`, `map_id_obj_unop`, `map_obj`, `op_map_id_obj`, `val_apply`, `functorNhds_map`, `functorNhds_obj_coe`	20
Total	35

IsOpenMap

Definitions

Name	Category	Theorems
`adjunctionNhds` 📖	CompOp	—
`functorNhds` 📖	CompOp	2 math math: `functorNhds_obj_coe`, `functorNhds_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functorNhds_map` 📖	mathematical	`IsOpenMap` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier`	`CategoryTheory.Functor.map` `TopologicalSpace.OpenNhds` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `functorNhds` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instPartialOrder` `functor` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	—	—
`functorNhds_obj_coe` 📖	mathematical	`IsOpenMap` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier`	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `CategoryTheory.Functor.obj` `TopologicalSpace.OpenNhds` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `functorNhds` `TopologicalSpace.Opens.instPartialOrder` `functor`	—	—

TopologicalSpace

Definitions

Name	Category	Theorems
`OpenNhds` 📖	CompOp	36 math math: `OpenNhds.coe_id`, `smoothSheafCommRing.ι_forgetStalk_inv`, `OpenNhds.inclusionMapIso_hom`, `smoothSheafCommRing.ι_evalHom_apply`, `OpenNhds.comp_apply`, `OpenNhds.val_apply`, `OpenNhds.inclusionMapIso_inv`, `IsOpenMap.functorNhds_obj_coe`, `skyscraperPresheafCocone_pt`, `smoothSheaf.ι_evalHom_apply`, `smoothSheaf.ι_evalHom_assoc`, `OpenNhds.map_obj`, `OpenNhds.op_map_id_obj`, `smoothSheafCommRing.ι_evalHom`, `OpenNhds.id_apply`, `OpenNhds.map_id_obj_unop`, `smoothSheafCommRing.ι_forgetStalk_inv_apply`, `smoothSheafCommRing.ι_forgetStalk_inv_assoc`, `skyscraperPresheafCocone_ι_app`, `IsOpenMap.functorNhds_map`, `OpenNhds.inclusion_obj`, `smoothSheafCommRing.ι_forgetStalk_hom_apply`, `OpenNhds.map_id_obj'`, `Topology.IsInducing.functorNhds_obj_coe`, `smoothSheafCommRing.ι_forgetStalk_hom_assoc`, `smoothSheaf.ι_evalHom`, `smoothSheafCommRing.ι_evalHom_assoc`, `smoothSheafCommRing.ι_forgetStalk_hom`, `skyscraperPresheafCoconeOfSpecializes_ι_app`, `OpenNhds.map_id_obj`, `AlgebraicGeometry.Scheme.affineBasisCover_map_range`, `skyscraperPresheafCoconeOfSpecializes_pt`, `OpenNhds.inclusionMapIso_inv_app`, `OpenNhds.apply_mk`, `OpenNhds.inclusionMapIso_hom_app`, `Topology.IsInducing.functorNhds_map`

TopologicalSpace.OpenNhds

Definitions

Name	Category	Theorems
`inclusion` 📖	CompOp	21 math math: `smoothSheafCommRing.ι_forgetStalk_inv`, `inclusionMapIso_hom`, `smoothSheafCommRing.ι_evalHom_apply`, `inclusionMapIso_inv`, `skyscraperPresheafCocone_pt`, `smoothSheaf.ι_evalHom_apply`, `smoothSheaf.ι_evalHom_assoc`, `smoothSheafCommRing.ι_evalHom`, `smoothSheafCommRing.ι_forgetStalk_inv_apply`, `smoothSheafCommRing.ι_forgetStalk_inv_assoc`, `skyscraperPresheafCocone_ι_app`, `inclusion_obj`, `smoothSheafCommRing.ι_forgetStalk_hom_apply`, `smoothSheafCommRing.ι_forgetStalk_hom_assoc`, `smoothSheaf.ι_evalHom`, `smoothSheafCommRing.ι_evalHom_assoc`, `smoothSheafCommRing.ι_forgetStalk_hom`, `skyscraperPresheafCoconeOfSpecializes_ι_app`, `skyscraperPresheafCoconeOfSpecializes_pt`, `inclusionMapIso_inv_app`, `inclusionMapIso_hom_app`
`inclusionMapIso` 📖	CompOp	4 math math: `inclusionMapIso_hom`, `inclusionMapIso_inv`, `inclusionMapIso_inv_app`, `inclusionMapIso_hom_app`
`infLELeft` 📖	CompOp	—
`infLERight` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instOrderTop` 📖	CompOp	—
`map` 📖	CompOp	9 math math: `inclusionMapIso_hom`, `inclusionMapIso_inv`, `map_obj`, `op_map_id_obj`, `map_id_obj_unop`, `map_id_obj'`, `map_id_obj`, `inclusionMapIso_inv_app`, `inclusionMapIso_hom_app`
`partialOrder` 📖	CompOp	35 math math: `coe_id`, `smoothSheafCommRing.ι_forgetStalk_inv`, `inclusionMapIso_hom`, `smoothSheafCommRing.ι_evalHom_apply`, `comp_apply`, `val_apply`, `inclusionMapIso_inv`, `IsOpenMap.functorNhds_obj_coe`, `skyscraperPresheafCocone_pt`, `smoothSheaf.ι_evalHom_apply`, `smoothSheaf.ι_evalHom_assoc`, `map_obj`, `op_map_id_obj`, `smoothSheafCommRing.ι_evalHom`, `id_apply`, `map_id_obj_unop`, `smoothSheafCommRing.ι_forgetStalk_inv_apply`, `smoothSheafCommRing.ι_forgetStalk_inv_assoc`, `skyscraperPresheafCocone_ι_app`, `IsOpenMap.functorNhds_map`, `inclusion_obj`, `smoothSheafCommRing.ι_forgetStalk_hom_apply`, `map_id_obj'`, `Topology.IsInducing.functorNhds_obj_coe`, `smoothSheafCommRing.ι_forgetStalk_hom_assoc`, `smoothSheaf.ι_evalHom`, `smoothSheafCommRing.ι_evalHom_assoc`, `smoothSheafCommRing.ι_forgetStalk_hom`, `skyscraperPresheafCoconeOfSpecializes_ι_app`, `map_id_obj`, `skyscraperPresheafCoconeOfSpecializes_pt`, `inclusionMapIso_inv_app`, `apply_mk`, `inclusionMapIso_hom_app`, `Topology.IsInducing.functorNhds_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mk` 📖	mathematical	`TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`DFunLike.coe` `Quiver.Hom` `TopologicalSpace.OpenNhds` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `opensNhds.instFunLike` `Quiver.Hom.le`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `Quiver.Hom` `TopologicalSpace.OpenNhds` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `opensNhds.instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `Quiver.Hom` `TopologicalSpace.OpenNhds` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `opensNhds.instFunLike` `CategoryTheory.CategoryStruct.comp`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `Quiver.Hom` `TopologicalSpace.OpenNhds` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `opensNhds.instFunLike`	—	—
`inclusionMapIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `TopologicalSpace.OpenNhds` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `inclusion` `TopologicalSpace.Opens.map` `map` `inclusionMapIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`inclusionMapIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `TopologicalSpace.OpenNhds` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.comp` `inclusion` `TopologicalSpace.Opens.map` `map` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inclusionMapIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`inclusionMapIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `TopologicalSpace.OpenNhds` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `inclusion` `TopologicalSpace.Opens.map` `map` `inclusionMapIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`inclusionMapIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `TopologicalSpace.OpenNhds` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.comp` `map` `inclusion` `TopologicalSpace.Opens.map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inclusionMapIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`inclusion_obj` 📖	mathematical	`TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`CategoryTheory.Functor.obj` `TopologicalSpace.OpenNhds` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `TopologicalSpace.Opens.instPartialOrder` `inclusion`	—	—
`isOpenEmbedding` 📖	mathematical	—	`Topology.IsOpenEmbedding` `TopCat.carrier` `CategoryTheory.Functor.obj` `TopologicalSpace.Opens` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat` `TopCat.instCategory` `TopologicalSpace.Opens.toTopCat` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `TopologicalSpace.Opens.inclusion'`	—	`TopologicalSpace.Opens.isOpenEmbedding`
`map_id_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `TopologicalSpace.OpenNhds` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `map`	—	—
`map_id_obj'` 📖	mathematical	`IsOpen` `TopCat.carrier` `TopCat.str` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.obj` `TopologicalSpace.OpenNhds` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `map`	—	—
`map_id_obj_unop` 📖	mathematical	—	`CategoryTheory.Functor.obj` `TopologicalSpace.OpenNhds` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `map` `Opposite.unop`	—	—
`map_obj` 📖	mathematical	`TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier`	`CategoryTheory.Functor.obj` `TopologicalSpace.OpenNhds` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `map` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map`	—	—
`op_map_id_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.OpenNhds` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `CategoryTheory.Functor.op` `map`	—	—
`val_apply` 📖	mathematical	—	`TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `DFunLike.coe` `Quiver.Hom` `TopologicalSpace.OpenNhds` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `partialOrder` `opensNhds.instFunLike`	—	—

TopologicalSpace.OpenNhds.opensNhds

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	5 math math: `TopologicalSpace.OpenNhds.coe_id`, `TopologicalSpace.OpenNhds.comp_apply`, `TopologicalSpace.OpenNhds.val_apply`, `TopologicalSpace.OpenNhds.id_apply`, `TopologicalSpace.OpenNhds.apply_mk`

Topology.IsInducing

Definitions

Name	Category	Theorems
`adjunctionNhds` 📖	CompOp	—
`functorNhds` 📖	CompOp	2 math math: `functorNhds_obj_coe`, `functorNhds_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functorNhds_map` 📖	mathematical	`Topology.IsInducing` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier`	`CategoryTheory.Functor.map` `TopologicalSpace.OpenNhds` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `functorNhds` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instPartialOrder` `functor`	—	—
`functorNhds_obj_coe` 📖	mathematical	`Topology.IsInducing` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier`	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `CategoryTheory.Functor.obj` `TopologicalSpace.OpenNhds` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.OpenNhds.partialOrder` `functorNhds` `TopologicalSpace.Opens.instPartialOrder` `functor`	—	—

---

← Back to Index