Documentation Verification Report

OpenMapping

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

Statistics

Metric	Count
Definitions	0
Theorems `isOpenMap_of_sigmaCompact`, `isOpenMap_of_sigmaCompact`, `isOpenMap_smul_of_sigmaCompact`, `isOpenMap_vadd_of_sigmaCompact`, `smul_singleton_mem_nhds_of_sigmaCompact`, `vadd_singleton_mem_nhds_of_sigmaCompact`	6
Total	6

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenMap_of_sigmaCompact` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `Continuous`	`IsOpenMap`	—	`AddAction.continuousVAdd_compHom` `ContinuousAdd.to_continuousVAdd` `AddAction.isPretransitive_compHom` `AddAction.Regular.isPretransitive` `add_zero` `isOpenMap_vadd_of_sigmaCompact`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenMap_of_sigmaCompact` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `Continuous`	`IsOpenMap`	—	`MulAction.continuousSMul_compHom` `ContinuousMul.to_continuousSMul` `MulAction.isPretransitive_compHom` `MulAction.Regular.isPretransitive` `mul_one` `isOpenMap_smul_of_sigmaCompact`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenMap_smul_of_sigmaCompact` 📖	mathematical	—	`IsOpenMap` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`smul_smul` `inv_mul_cancel_right` `Set.image_comp` `Set.smul_singleton` `smul_singleton_mem_nhds_of_sigmaCompact` `Set.image_mul_right` `inv_inv` `mul_inv_cancel` `IsOpenMap.image_mem_nhds` `isOpenMap_mul_right` `IsTopologicalGroup.toContinuousMul`
`isOpenMap_vadd_of_sigmaCompact` 📖	mathematical	—	`IsOpenMap` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`isOpenMap_iff_nhds_le` `Filter.le_map_iff` `vadd_vadd` `neg_add_cancel_right` `Set.image_comp` `Set.vadd_singleton` `vadd_singleton_mem_nhds_of_sigmaCompact` `Set.image_add_right` `neg_neg` `add_neg_cancel` `IsOpenMap.image_mem_nhds` `isOpenMap_add_right` `IsTopologicalAddGroup.toContinuousAdd`
`smul_singleton_mem_nhds_of_sigmaCompact` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.instSingletonSet`	—	`exists_closed_nhds_one_inv_eq_mul_subset` `countable_cover_nhds_of_sigmaCompact` `IsScalarTower.continuousConstSMul` `IsScalarTower.left` `IsTopologicalGroup.toContinuousMul` `nonempty_interior_of_iUnion_of_closed` `instCountableProd` `instCountableNat` `Encodable.countable` `IsCompact.isClosed` `IsCompact.image` `IsCompact.inter_right` `isCompact_compactCovering` `IsClosed.smul` `Continuous.smul` `continuous_id'` `continuous_const` `Set.smul_singleton` `Set.eq_univ_iff_forall` `MulAction.exists_smul_eq` `exists_mem_compactCovering` `Set.exists_set_mem_of_union_eq_top` `Set.Nonempty.mono` `interior_mono` `Set.smul_subset_smul_right` `Set.inter_subset_right` `Set.smul_set_nonempty` `interior_smul` `ContinuousSMul.continuousConstSMul` `smul_assoc` `Set.isScalarTower'` `interior_subset` `mem_interior_iff_mem_nhds` `Set.mem_inv_smul_set_iff` `Set.Subset.trans` `Set.smul_set_subset_smul` `Set.inv_mem_inv` `Filter.mem_of_superset`
`vadd_singleton_mem_nhds_of_sigmaCompact` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`HVAdd.hVAdd` `instHVAdd` `Set.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.instSingletonSet`	—	`exists_closed_nhds_zero_neg_eq_add_subset` `countable_cover_nhds_of_sigmaCompact` `vadd_mem_nhds_self` `VAddAssocClass.continuousConstVAdd` `VAddAssocClass.left` `IsTopologicalAddGroup.toContinuousAdd` `nonempty_interior_of_iUnion_of_closed` `instCountableProd` `instCountableNat` `Encodable.countable` `IsCompact.isClosed` `IsCompact.image` `IsCompact.inter_right` `isCompact_compactCovering` `IsClosed.vadd` `Continuous.vadd` `continuous_id'` `continuous_const` `Set.vadd_singleton` `Set.eq_univ_iff_forall` `AddAction.exists_vadd_eq` `exists_mem_compactCovering` `Set.exists_set_mem_of_union_eq_top` `Set.mem_iUnion` `Set.mem_image` `Set.mem_inter_iff` `Set.Nonempty.mono` `interior_mono` `Set.vadd_subset_vadd_right` `Set.inter_subset_right` `Set.vadd_set_nonempty` `interior_vadd` `ContinuousVAdd.continuousConstVAdd` `vadd_assoc` `Set.vaddAssocClass'` `interior_subset` `mem_interior_iff_mem_nhds` `Set.mem_neg_vadd_set_iff` `Set.Subset.trans` `Set.vadd_set_subset_vadd` `Set.neg_mem_neg` `Filter.mem_of_superset`

---

← Back to Index