Documentation Verification Report

Product

📁 Source: Mathlib/Topology/Homotopy/Product.lean

Statistics

Metric	Count
Definitions `prod`, `pi`, `prod`, `Product`, `Product`, `pi`, `piHomotopy`, `prod`, `prodHomotopy`, `proj`, `projLeft`, `projRight`	12
Theorems `prod_apply`, `pi_apply`, `prod_apply`, `comp_pi_eq_pi_comp`, `comp_prod_eq_prod_comp`, `pi_lift`, `pi_proj`, `prod_lift`, `prod_projLeft_projRight`, `projLeft_prod`, `projRight_prod`, `proj_pi`	12
Total	24

ContinuousMap.Homotopy

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	1 math math: `prod_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap.Homotopy` `instTopologicalSpaceProd` `ContinuousMap.prodMk` `Set.Elem` `Real` `unitInterval` `instFunLike` `prod`	—	—

ContinuousMap.HomotopyRel

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	1 math math: `pi_apply`
`prod` 📖	CompOp	1 math math: `prod_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap.HomotopyWith` `Pi.topologicalSpace` `ContinuousMap.pi` `Set.Elem` `Real` `unitInterval` `ContinuousMap.HomotopyWith.instFunLike` `pi`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap.HomotopyWith` `instTopologicalSpaceProd` `ContinuousMap.prodMk` `Set.Elem` `Real` `unitInterval` `ContinuousMap.HomotopyWith.instFunLike` `prod`	—	—

DihedralGroup

Definitions

Name	Category	Theorems
`Product` 📖	CompOp	3 math math: `commProb_nil`, `commProb_cons`, `commProb_reciprocal`

Filter

Definitions

Name	Category	Theorems
`Product` 📖	CompOp	2 math math: `FirstOrder.Language.Ultraproduct.Product.instNonempty`, `FirstOrder.Language.Ultraproduct.sentence_realize`

Path.Homotopic

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	5 math math: `comp_pi_eq_pi_comp`, `pi_proj`, `FundamentalGroupoidFunctor.piToPiTop_map`, `pi_lift`, `proj_pi`
`piHomotopy` 📖	CompOp	—
`prod` 📖	CompOp	6 math math: `prod_projLeft_projRight`, `projRight_prod`, `projLeft_prod`, `prod_lift`, `comp_prod_eq_prod_comp`, `FundamentalGroupoidFunctor.prodToProdTop_map`
`prodHomotopy` 📖	CompOp	—
`proj` 📖	CompOp	3 math math: `pi_proj`, `FundamentalGroupoidFunctor.proj_map`, `proj_pi`
`projLeft` 📖	CompOp	3 math math: `prod_projLeft_projRight`, `FundamentalGroupoidFunctor.projLeft_map`, `projLeft_prod`
`projRight` 📖	CompOp	3 math math: `prod_projLeft_projRight`, `projRight_prod`, `FundamentalGroupoidFunctor.projRight_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_pi_eq_pi_comp` 📖	mathematical	—	`Quotient.trans` `Pi.topologicalSpace` `pi`	—	`Quotient.induction_on_pi` `pi_lift` `Quotient.mk_trans` `Path.trans_pi_eq_pi_trans`
`comp_prod_eq_prod_comp` 📖	mathematical	—	`Quotient.trans` `instTopologicalSpaceProd` `prod`	—	`Quotient.ind₂` `Path.trans_prod_eq_prod_trans`
`pi_lift` 📖	mathematical	—	`pi` `Pi.topologicalSpace` `Path.pi`	—	`Quotient.map.congr_simp` `Quotient.choice_eq`
`pi_proj` 📖	mathematical	—	`pi` `proj`	—	`continuous_apply` `ContinuousMap.continuous` `pi_lift`
`prod_lift` 📖	mathematical	—	`prod` `instTopologicalSpaceProd` `Path.prod`	—	—
`prod_projLeft_projRight` 📖	mathematical	—	`prod` `projLeft` `projRight`	—	`Quotient.ind` `continuous_fst` `ContinuousMap.continuous` `continuous_snd`
`projLeft_prod` 📖	mathematical	—	`projLeft` `prod`	—	`Quotient.ind₂` `continuous_fst` `projLeft.eq_1` `prod_lift` `ContinuousMap.continuous` `Quotient.mk_map`
`projRight_prod` 📖	mathematical	—	`projRight` `prod`	—	`Quotient.ind₂` `continuous_snd` `projRight.eq_1` `prod_lift` `ContinuousMap.continuous` `Quotient.mk_map`
`proj_pi` 📖	mathematical	—	`proj` `pi`	—	`Quotient.induction_on_pi` `continuous_apply` `proj.eq_1` `pi_lift`

---

← Back to Index