Documentation Verification Report

Open

📁 Source: Mathlib/Topology/Hom/Open.lean

Statistics

Metric	Count
Definitions `ContinuousOpenMap`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `toContinuousMap`, `ContinuousOpenMapClass`, `instCoeTCContinuousOpenMapOfContinuousOpenMapClass`, `«term_→CO_»`	10
Theorems `cancel_left`, `cancel_right`, `coe_comp`, `coe_copy`, `coe_id`, `coe_toContinuousMap`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instContinuousOpenMapClass`, `map_open'`, `toFun_eq_coe`, `map_open`, `toContinuousMapClass`	19
Total	29

ContinuousOpenMap

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	7 math math: `comp_apply`, `cancel_right`, `cancel_left`, `comp_id`, `coe_comp`, `id_comp`, `comp_assoc`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`id` 📖	CompOp	4 math math: `id_apply`, `coe_id`, `comp_id`, `id_comp`
`instFunLike` 📖	CompOp	8 math math: `id_apply`, `comp_apply`, `toFun_eq_coe`, `ext_iff`, `coe_id`, `coe_toContinuousMap`, `instContinuousOpenMapClass`, `coe_comp`
`instInhabited` 📖	CompOp	—
`toContinuousMap` 📖	CompOp	3 math math: `toFun_eq_coe`, `coe_toContinuousMap`, `map_open'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `ContinuousOpenMap` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `ContinuousOpenMap` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousOpenMap` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `ContinuousOpenMap` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `ContinuousOpenMap` `instFunLike` `id`	—	—
`coe_toContinuousMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toContinuousMap` `ContinuousOpenMap` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousOpenMap` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `ContinuousOpenMap` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `ContinuousOpenMap` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousOpenMap` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousOpenMap` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instContinuousOpenMapClass` 📖	mathematical	—	`ContinuousOpenMapClass` `ContinuousOpenMap` `instFunLike`	—	`ContinuousMap.continuous_toFun` `map_open'`
`map_open'` 📖	mathematical	—	`IsOpenMap` `ContinuousMap.toFun` `toContinuousMap`	—	—
`toFun_eq_coe` 📖	mathematical	—	`ContinuousMap.toFun` `toContinuousMap` `DFunLike.coe` `ContinuousOpenMap` `instFunLike`	—	—

ContinuousOpenMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_open` 📖	mathematical	—	`IsOpenMap` `DFunLike.coe`	—	—
`toContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass`	—	—

(root)

Definitions

Name	Category	Theorems
`ContinuousOpenMap` 📖	CompData	8 math math: `ContinuousOpenMap.id_apply`, `ContinuousOpenMap.comp_apply`, `ContinuousOpenMap.toFun_eq_coe`, `ContinuousOpenMap.ext_iff`, `ContinuousOpenMap.coe_id`, `ContinuousOpenMap.coe_toContinuousMap`, `ContinuousOpenMap.instContinuousOpenMapClass`, `ContinuousOpenMap.coe_comp`
`ContinuousOpenMapClass` 📖	CompData	1 math math: `ContinuousOpenMap.instContinuousOpenMapClass`
`instCoeTCContinuousOpenMapOfContinuousOpenMapClass` 📖	CompOp	—
`«term_→CO_»` 📖	CompOp	—

---

← Back to Index