Documentation Verification Report

Group

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

Statistics

Metric	Count
Definitions	0
Theorems `abs`, `mabs`, `abs`, `mabs`, `abs`, `mabs`, `abs`, `mabs`, `abs`, `mabs`, `toIsTopologicalAddGroup`, `toIsTopologicalGroup`, `comap_abs_nhds_zero`, `comap_mabs_nhds_one`, `continuous_abs`, `continuous_mabs`, `denseRange_zpow_iff_surjective`, `denseRange_zsmul_iff_surjective`, `not_denseRange_zpow`, `not_denseRange_zsmul`, `tendsto_abs_nhdsNE_zero`, `tendsto_mabs_nhdsNE_one`, `tendsto_one_iff_mabs_tendsto_one`, `tendsto_zero_iff_abs_tendsto_zero`	24
Total	24

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`Continuous`	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup`	—	`comp` `continuous_abs`
`mabs` 📖	mathematical	`Continuous`	`mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup`	—	`comp` `continuous_mabs`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`ContinuousAt`	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup`	—	`Filter.Tendsto.abs`
`mabs` 📖	mathematical	`ContinuousAt`	`mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup`	—	`Filter.Tendsto.mabs`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`ContinuousOn`	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup`	—	`ContinuousWithinAt.abs`
`mabs` 📖	mathematical	`ContinuousOn`	`mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup`	—	`ContinuousWithinAt.mabs`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`ContinuousWithinAt`	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup`	—	`Filter.Tendsto.abs`
`mabs` 📖	mathematical	`ContinuousWithinAt`	`mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup`	—	`Filter.Tendsto.mabs`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`Filter.Tendsto` `nhds`	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup`	—	`comp` `Continuous.tendsto` `continuous_abs`
`mabs` 📖	mathematical	`Filter.Tendsto` `nhds`	`mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup`	—	`comp` `Continuous.tendsto` `continuous_mabs`

LinearOrderedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup`	—	`continuous_iff_continuousAt` `tendsto_nhds` `dense_or_discrete` `Filter.mp_mem` `Filter.Eventually.prod_nhds` `eventually_abs_sub_lt` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Filter.univ_mem'` `sub_add_sub_comm` `abs_add_le` `add_lt_add_of_lt_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_sub_cancel` `Filter.Eventually.mono` `abs_sub_nonpos` `add_sub_add_right_eq_sub` `sub_self` `abs_zero` `neg_sub_neg` `abs_sub_comm`

LinearOrderedCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsTopologicalGroup` 📖	mathematical	—	`IsTopologicalGroup` `CommGroup.toGroup`	—	`dense_or_discrete` `Filter.mp_mem` `Filter.Eventually.prod_nhds` `eventually_mabs_div_lt` `one_lt_div'` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `RightCancelSemigroup.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `Filter.univ_mem'` `div_mul_div_comm` `mabs_mul_le` `mul_lt_mul_of_lt_of_lt` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `mul_div_cancel` `Filter.Eventually.mono` `mabs_div_le_one` `mul_div_mul_right_eq_div` `div_self'` `mabs_one` `continuous_iff_continuousAt` `tendsto_nhds` `inv_div_inv` `mabs_div_comm`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_abs_nhds_zero` 📖	mathematical	—	`Filter.comap` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`nhds_eq_iInf_abs_sub` `iInf_congr_Prop` `zero_sub` `abs_neg` `Filter.comap_iInf` `Filter.comap_principal` `abs_abs` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`comap_mabs_nhds_one` 📖	mathematical	—	`Filter.comap` `mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`nhds_eq_iInf_mabs_div` `iInf_congr_Prop` `one_div` `mabs_inv` `Filter.comap_iInf` `Filter.comap_principal` `mabs_mabs` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul`
`continuous_abs` 📖	mathematical	—	`Continuous` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup`	—	`Continuous.max` `OrderTopology.to_orderClosedTopology` `continuous_id` `ContinuousNeg.continuous_neg` `IsTopologicalAddGroup.toContinuousNeg` `LinearOrderedAddCommGroup.toIsTopologicalAddGroup`
`continuous_mabs` 📖	mathematical	—	`Continuous` `mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup`	—	`Continuous.max` `OrderTopology.to_orderClosedTopology` `continuous_id` `ContinuousInv.continuous_inv` `IsTopologicalGroup.toContinuousInv` `LinearOrderedCommGroup.toIsTopologicalGroup`
`denseRange_zpow_iff_surjective` 📖	mathematical	—	`DenseRange` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono` `contravariant_lt_of_covariant_le` `DenseRange.exists_mem_open` `isOpen_Ioo` `OrderTopology.to_orderClosedTopology` `eq_or_ne` `Ne.lt_or_gt` `zpow_add` `zpow_one` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `RightCancelSemigroup.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul` `contravariant_swap_mul_of_contravariant_mul` `zpow_sub` `div_lt_iff_lt_mul` `zpow_lt_zpow_iff_right` `LE.le.eq_or_lt` `one_zpow` `Set.range_const` `closure_singleton` `T2Space.t1Space` `OrderClosedTopology.to_t2Space` `zpow_neg` `Function.Surjective.range_comp` `neg_surjective` `Function.Surjective.denseRange`
`denseRange_zsmul_iff_surjective` 📖	mathematical	—	`DenseRange` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Set.mem_Ioo` `lt_add_iff_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `contravariant_lt_of_covariant_le` `DenseRange.exists_mem_open` `isOpen_Ioo` `OrderTopology.to_orderClosedTopology` `eq_or_ne` `Ne.lt_or_gt` `add_zsmul` `one_zsmul` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `contravariant_swap_add_of_contravariant_add` `sub_zsmul` `sub_eq_add_neg` `lt_sub_iff_add_lt` `sub_lt_iff_lt_add` `zsmul_lt_zsmul_iff_left` `Set.range_eq_univ` `LE.le.eq_or_lt` `not_lt` `zsmul_zero` `Set.range_const` `dense_iff_closure_eq` `closure_singleton` `T2Space.t1Space` `OrderClosedTopology.to_t2Space` `neg_zsmul` `zsmul_neg` `Function.Surjective.range_comp` `neg_surjective` `neg_pos` `Function.Surjective.denseRange`
`not_denseRange_zpow` 📖	mathematical	—	`DenseRange` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`Iff.not` `denseRange_zpow_iff_surjective` `not_isCyclic_of_denselyOrdered`
`not_denseRange_zsmul` 📖	mathematical	—	`DenseRange` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Iff.not` `denseRange_zsmul_iff_surjective` `not_isAddCyclic_of_denselyOrdered`
`tendsto_abs_nhdsNE_zero` 📖	mathematical	—	`Filter.Tendsto` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup` `nhdsWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`Filter.Tendsto.inf` `Continuous.tendsto'` `continuous_abs` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Filter.tendsto_principal_principal` `abs_pos`
`tendsto_mabs_nhdsNE_one` 📖	mathematical	—	`Filter.Tendsto` `mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup` `nhdsWithin` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`Filter.Tendsto.inf` `Continuous.tendsto'` `continuous_mabs` `mabs_one` `IsOrderedMonoid.toMulLeftMono` `Filter.tendsto_principal_principal` `one_lt_mabs`
`tendsto_one_iff_mabs_tendsto_one` 📖	mathematical	—	`Filter.Tendsto` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup`	—	`Filter.tendsto_comap_iff` `comap_mabs_nhds_one`
`tendsto_zero_iff_abs_tendsto_zero` 📖	mathematical	—	`Filter.Tendsto` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup`	—	`Filter.tendsto_comap_iff` `comap_abs_nhds_zero`

---

← Back to Index