Documentation Verification Report

AddTorsor

📁 Source: Mathlib/Topology/Algebra/Group/AddTorsor.lean

Statistics

Metric	Count
Definitions `vaddConst`, `IsTopologicalAddTorsor`	2
Theorems `vsub`, `vsub`, `vsub`, `vsub`, `vsub`, `vaddConst_apply`, `vaddConst_symm_apply`, `continuous_vsub`, `toContinuousVAdd`, `to_isTopologicalAddGroup`, `instIsTopologicalAddTorsor`, `instIsTopologicalAddTorsorForall`, `instIsTopologicalAddTorsorProd`	13
Total	15

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vsub` 📖	mathematical	`Continuous`	`VSub.vsub` `AddTorsor.toVSub`	—	`comp₂` `IsTopologicalAddTorsor.continuous_vsub`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vsub` 📖	mathematical	`ContinuousAt`	`VSub.vsub` `AddTorsor.toVSub`	—	`Filter.Tendsto.vsub`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vsub` 📖	mathematical	`ContinuousOn`	`VSub.vsub` `AddTorsor.toVSub`	—	`ContinuousWithinAt.vsub`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vsub` 📖	mathematical	`ContinuousWithinAt`	`VSub.vsub` `AddTorsor.toVSub`	—	`Filter.Tendsto.vsub`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vsub` 📖	mathematical	`Filter.Tendsto` `nhds`	`VSub.vsub` `AddTorsor.toVSub` `Pi.addGroup` `Pi.instAddTorsor`	—	`comp` `Continuous.tendsto` `IsTopologicalAddTorsor.continuous_vsub` `prodMk_nhds`

Homeomorph

Definitions

Name	Category	Theorems
`vaddConst` 📖	CompOp	2 math math: `vaddConst_apply`, `vaddConst_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vaddConst_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `vaddConst` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	—
`vaddConst_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm` `vaddConst` `VSub.vsub` `AddTorsor.toVSub`	—	—

IsTopologicalAddTorsor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_vsub` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `VSub.vsub` `AddTorsor.toVSub`	—	—
`toContinuousVAdd` 📖	mathematical	—	`ContinuousVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	—
`to_isTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup`	—	`AddTorsor.nonempty` `vadd_vadd` `vadd_vsub` `Continuous.vsub` `Continuous.vadd` `toContinuousVAdd` `Continuous.fst` `continuous_id'` `Continuous.snd` `continuous_const` `vsub_vadd_eq_vsub_sub` `vsub_self` `zero_sub`

(root)

Definitions

Name	Category	Theorems
`IsTopologicalAddTorsor` 📖	CompData	4 math math: `instIsTopologicalAddTorsorProd`, `AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection`, `instIsTopologicalAddTorsor_1`, `instIsTopologicalAddTorsor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTopologicalAddTorsor` 📖	mathematical	—	`IsTopologicalAddTorsor` `addGroupIsAddTorsor`	—	`ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `Continuous.fst` `continuous_id'` `Continuous.snd`
`instIsTopologicalAddTorsorForall` 📖	mathematical	`IsTopologicalAddTorsor` `AddCommGroup.toAddGroup`	`Pi.addGroup` `Pi.topologicalSpace` `Pi.instAddTorsor`	—	`continuous_pi` `Continuous.vadd` `IsTopologicalAddTorsor.toContinuousVAdd` `Continuous.comp'` `continuous_apply` `Continuous.fst` `continuous_id'` `Continuous.snd` `Continuous.vsub`
`instIsTopologicalAddTorsorProd` 📖	mathematical	—	`IsTopologicalAddTorsor` `Prod.instAddGroup` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `Prod.instAddTorsor`	—	`Continuous.prodMk` `Continuous.vadd` `IsTopologicalAddTorsor.toContinuousVAdd` `Continuous.fst` `continuous_id'` `Continuous.snd` `Continuous.vsub`

---

← Back to Index