Documentation Verification Report

Affine

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

Statistics

Metric	Count
Definitions	0
Theorems `continuous_iff`, `continuous_linear_iff`, `homothety_continuous`, `homothety_isOpenMap`, `isOpenMap_linear_iff`, `lineMap_continuous`, `lineMap_continuous_uncurry`, `lineMap`, `lineMap`, `lineMap`, `lineMap`, `lineMap`, `midpoint`, `eventually_homothety_image_subset_of_finite_subset_interior`, `eventually_homothety_mem_of_mem_interior`	15
Total	15

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_iff` 📖	mathematical	—	`Continuous` `DFunLike.coe` `AffineMap` `instFunLike` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `linear`	—	`continuous_linear_iff`
`continuous_linear_iff` 📖	mathematical	—	`Continuous` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `linear` `AffineMap` `instFunLike`	—	`AddTorsor.nonempty` `map_vadd` `vadd_vsub`
`homothety_continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `AffineMap` `CommRing.toRing` `instFunLike` `homothety`	—	`coe_homothety` `Continuous.vadd` `IsTopologicalAddTorsor.toContinuousVAdd` `Continuous.const_smul` `Continuous.vsub` `continuous_id'` `continuous_const`
`homothety_isOpenMap` 📖	mathematical	—	`IsOpenMap` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Field.toCommRing` `instFunLike` `homothety`	—	`IsOpenMap.of_inverse` `homothety_continuous` `mul_inv_cancel₀` `homothety_one` `inv_mul_cancel₀`
`isOpenMap_linear_iff` 📖	mathematical	—	`IsOpenMap` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `linear` `AffineMap` `instFunLike`	—	`AddTorsor.nonempty` `map_vadd` `vadd_vsub`
`lineMap_continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instFunLike` `lineMap`	—	`Continuous.comp'` `lineMap_continuous_uncurry` `Continuous.prodMk` `continuous_const` `continuous_id'`
`lineMap_continuous_uncurry` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instFunLike` `lineMap`	—	`Continuous.vadd` `IsTopologicalAddTorsor.toContinuousVAdd` `Continuous.smul` `Continuous.snd` `continuous_id'` `Continuous.vsub` `Continuous.fst`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineMap` 📖	mathematical	`Continuous`	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`comp'` `AffineMap.lineMap_continuous_uncurry` `prodMk`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineMap` 📖	mathematical	`ContinuousAt`	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`comp'` `Continuous.continuousAt` `AffineMap.lineMap_continuous_uncurry` `prodMk`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineMap` 📖	mathematical	`ContinuousOn`	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`Continuous.comp_continuousOn'` `AffineMap.lineMap_continuous_uncurry` `prodMk`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineMap` 📖	mathematical	`ContinuousWithinAt`	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`Filter.Tendsto.lineMap`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineMap` 📖	mathematical	`Filter.Tendsto` `nhds`	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`vadd` `IsTopologicalAddTorsor.toContinuousVAdd` `smul` `vsub`
`midpoint` 📖	mathematical	`Filter.Tendsto` `nhds`	`midpoint`	—	`Nat.instAtLeastTwoHAddOfNat` `lineMap` `tendsto_const_nhds`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_homothety_image_subset_of_finite_subset_interior` 📖	mathematical	`Set` `Set.instHasSubset` `interior`	`Filter.Eventually` `Set.image` `DFunLike.coe` `AffineMap` `CommRing.toRing` `AffineMap.instFunLike` `AffineMap.homothety` `nhds` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`eventually_homothety_mem_of_mem_interior` `Filter.eventually_all_finite`
`eventually_homothety_mem_of_mem_interior` 📖	mathematical	`Set` `Set.instMembership` `interior`	`Filter.Eventually` `DFunLike.coe` `AffineMap` `CommRing.toRing` `AffineMap.instFunLike` `AffineMap.homothety` `nhds` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`AffineMap.lineMap_continuous` `Filter.mp_mem` `Filter.Tendsto.eventually` `Continuous.tendsto'` `AffineMap.homothety_one` `IsOpen.eventually_mem` `isOpen_interior` `Filter.univ_mem'` `interior_subset`

---

← Back to Index