Documentation Verification Report

Star

📁 Source: Mathlib/Topology/Algebra/Star.lean

Statistics

Metric	Count
Definitions `ContinuousStar`, `starContinuousMap`	2
Theorems `continuous_star`, `continuousAt_star`, `continuousOn_star`, `continuousWithinAt_star`, `instContinuousStarForall`, `instContinuousStarMulOpposite`, `instContinuousStarProd`, `instContinuousStarUnits`, `starContinuousMap_apply`, `tendsto_star`	10
Total	12

ContinuousStar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_star` 📖	mathematical	—	`Continuous` `Star.star`	—	—

(root)

Definitions

Name	Category	Theorems
`ContinuousStar` 📖	CompData	10 math math: `instContinuousStarMatrix`, `Complex.instContinuousStar`, `NormedStarGroup.to_continuousStar`, `RCLike.instContinuousStar`, `instContinuousStarUnits`, `instContinuousStarSubtypeMemSubmonoidUnitary`, `instContinuousStarProd`, `instContinuousStarReal`, `instContinuousStarMulOpposite`, `NNReal.instContinuousStar`
`starContinuousMap` 📖	CompOp	1 math math: `starContinuousMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_star` 📖	mathematical	—	`ContinuousAt` `Star.star`	—	`Continuous.continuousAt` `ContinuousStar.continuous_star`
`continuousOn_star` 📖	mathematical	—	`ContinuousOn` `Star.star`	—	`Continuous.continuousOn` `ContinuousStar.continuous_star`
`continuousWithinAt_star` 📖	mathematical	—	`ContinuousWithinAt` `Star.star`	—	`Continuous.continuousWithinAt` `ContinuousStar.continuous_star`
`instContinuousStarForall` 📖	mathematical	`ContinuousStar`	`Pi.topologicalSpace` `Pi.instStarForall`	—	`continuous_pi` `Continuous.star` `continuous_apply`
`instContinuousStarMulOpposite` 📖	mathematical	—	`ContinuousStar` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.instStar`	—	`Continuous.comp` `MulOpposite.continuous_op` `Continuous.star` `MulOpposite.continuous_unop`
`instContinuousStarProd` 📖	mathematical	—	`ContinuousStar` `instTopologicalSpaceProd` `Prod.instStar`	—	`Continuous.prodMk` `Continuous.comp` `ContinuousStar.continuous_star` `continuous_fst` `continuous_snd`
`instContinuousStarUnits` 📖	mathematical	—	`ContinuousStar` `Units` `Units.instTopologicalSpaceUnits` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Units.instMul` `Units.instStarMul`	—	`continuous_induced_rng` `Continuous.star` `instContinuousStarProd` `instContinuousStarMulOpposite` `Units.continuous_embedProduct`
`starContinuousMap_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `starContinuousMap` `Star.star`	—	—
`tendsto_star` 📖	mathematical	—	`Filter.Tendsto` `Star.star` `nhds`	—	`continuousAt_star`

---

← Back to Index