Documentation Verification Report

Constructions

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

Statistics

Metric	Count
Definitions `instTopologicalSpaceAddOpposite`, `opHomeomorph`, `instTopologicalSpaceAddUnits`, `instTopologicalSpaceMulOpposite`, `opHomeomorph`, `instTopologicalSpaceUnits`	6
Theorems `comap_op_nhds`, `comap_unop_nhds`, `continuous_op`, `continuous_unop`, `instCompactSpace`, `instDiscreteTopology`, `instLocallyCompactSpace`, `instT2Space`, `instWeaklyLocallyCompactSpace`, `map_op_nhds`, `map_unop_nhds`, `opHomeomorph_apply`, `opHomeomorph_symm_apply`, `continuous_coe_neg`, `continuous_embedProduct`, `continuous_iff`, `continuous_map`, `continuous_val`, `embedding_val_mk`, `instDiscreteTopology`, `instT2Space`, `isEmbedding_embedProduct`, `isEmbedding_val_mk'`, `isInducing_embedProduct`, `isOpenMap_map`, `topology_eq_inf`, `comap_op_nhds`, `comap_unop_nhds`, `continuous_op`, `continuous_unop`, `instCompactSpace`, `instDiscreteTopology`, `instLocallyCompactSpace`, `instT2Space`, `instWeaklyLocallyCompactSpace`, `map_op_nhds`, `map_unop_nhds`, `opHomeomorph_apply`, `opHomeomorph_symm_apply`, `continuous_coe_inv`, `continuous_embedProduct`, `continuous_iff`, `continuous_map`, `continuous_val`, `embedding_val_mk`, `instDiscreteTopology`, `instT2Space`, `isEmbedding_embedProduct`, `isEmbedding_val_mk'`, `isInducing_embedProduct`, `isOpenMap_map`, `topology_eq_inf`	52
Total	58

AddOpposite

Definitions

Name	Category	Theorems
`instTopologicalSpaceAddOpposite` 📖	CompOp	31 math math: `comap_op_leftUniformSpace`, `instT2Space`, `instContinuousAdd`, `instIsTopologicalRingAddOpposite`, `opHomeomorph_apply`, `continuousVAdd`, `comap_unop_nhds`, `continuous_op`, `continuous_unop`, `comap_op_nhds`, `instProperVAddAddOppositeOfIsTopologicalAddGroup`, `instIsTopologicalAddGroupAddOpposite`, `instCompactSpace`, `instContinuousMulAddOpposite`, `ContinuousAdd.to_continuousVAdd_op`, `instWeaklyLocallyCompactSpace`, `ContinuousVAdd.op`, `instIsTopologicalSemiringAddOpposite`, `instContinuousNegAddOpposite`, `map_unop_nhds`, `instDiscreteTopology`, `instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe`, `AddUnits.continuous_embedProduct`, `continuousConstVAdd`, `AddUnits.isClosedEmbedding_embedProduct`, `AddUnits.isEmbedding_embedProduct`, `AddUnits.isInducing_embedProduct`, `comap_op_rightUniformSpace`, `opHomeomorph_symm_apply`, `instLocallyCompactSpace`, `map_op_nhds`
`opHomeomorph` 📖	CompOp	2 math math: `opHomeomorph_apply`, `opHomeomorph_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_op_nhds` 📖	mathematical	—	`Filter.comap` `AddOpposite` `op` `nhds` `instTopologicalSpaceAddOpposite` `unop`	—	`Homeomorph.comap_nhds_eq`
`comap_unop_nhds` 📖	mathematical	—	`Filter.comap` `AddOpposite` `unop` `nhds` `instTopologicalSpaceAddOpposite` `op`	—	`Homeomorph.comap_nhds_eq`
`continuous_op` 📖	mathematical	—	`Continuous` `AddOpposite` `instTopologicalSpaceAddOpposite` `op`	—	`continuous_induced_rng` `continuous_id`
`continuous_unop` 📖	mathematical	—	`Continuous` `AddOpposite` `instTopologicalSpaceAddOpposite` `unop`	—	`continuous_induced_dom`
`instCompactSpace` 📖	mathematical	—	`CompactSpace` `AddOpposite` `instTopologicalSpaceAddOpposite`	—	`Homeomorph.compactSpace`
`instDiscreteTopology` 📖	mathematical	—	`DiscreteTopology` `AddOpposite` `instTopologicalSpaceAddOpposite`	—	`Topology.IsEmbedding.discreteTopology` `Homeomorph.isEmbedding`
`instLocallyCompactSpace` 📖	mathematical	—	`LocallyCompactSpace` `AddOpposite` `instTopologicalSpaceAddOpposite`	—	`Topology.IsClosedEmbedding.locallyCompactSpace` `Homeomorph.isClosedEmbedding`
`instT2Space` 📖	mathematical	—	`T2Space` `AddOpposite` `instTopologicalSpaceAddOpposite`	—	`Homeomorph.t2Space`
`instWeaklyLocallyCompactSpace` 📖	mathematical	—	`WeaklyLocallyCompactSpace` `AddOpposite` `instTopologicalSpaceAddOpposite`	—	`Topology.IsClosedEmbedding.weaklyLocallyCompactSpace` `Homeomorph.isClosedEmbedding`
`map_op_nhds` 📖	mathematical	—	`Filter.map` `AddOpposite` `op` `nhds` `instTopologicalSpaceAddOpposite`	—	`Homeomorph.map_nhds_eq`
`map_unop_nhds` 📖	mathematical	—	`Filter.map` `AddOpposite` `unop` `nhds` `instTopologicalSpaceAddOpposite`	—	`Homeomorph.map_nhds_eq`
`opHomeomorph_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `AddOpposite` `instTopologicalSpaceAddOpposite` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `opHomeomorph` `op`	—	—
`opHomeomorph_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `AddOpposite` `instTopologicalSpaceAddOpposite` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `opHomeomorph` `unop`	—	—

AddUnits

Definitions

Name	Category	Theorems
`instTopologicalSpaceAddUnits` 📖	CompOp	27 math math: `instContinuousAdd`, `Continuous.addUnits_map`, `continuous_val`, `instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousAdd`, `ContinuousMap.addUnitsLift_apply_neg_apply`, `isEmbedding_val_mk'`, `ContinuousMap.val_addUnitsLift_apply_apply`, `instDiscreteTopology`, `instT2Space`, `isEmbedding_val`, `continuousVAdd`, `ContinuousMap.val_addUnitsLift_symm_apply_apply`, `AddSubmonoid.isOpen_addUnits`, `instIsTopologicalAddGroupOfContinuousAdd`, `isOpenMap_map`, `embedding_val_mk`, `instLocallyCompactSpaceOfT1SpaceOfContinuousAdd`, `instCompactSpaceOfT1SpaceOfContinuousAdd`, `continuous_embedProduct`, `continuous_map`, `isClosedEmbedding_embedProduct`, `ContinuousMap.addUnitsLift_symm_apply_apply_neg'`, `topology_eq_inf`, `isEmbedding_embedProduct`, `isInducing_embedProduct`, `continuous_iff`, `continuous_coe_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_coe_neg` 📖	mathematical	—	`Continuous` `AddUnits` `instTopologicalSpaceAddUnits` `val` `instNeg`	—	`continuous_iff` `continuous_id`
`continuous_embedProduct` 📖	mathematical	—	`Continuous` `AddUnits` `AddOpposite` `instTopologicalSpaceAddUnits` `instTopologicalSpaceProd` `AddOpposite.instTopologicalSpaceAddOpposite` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddOpposite.instAddZeroClass` `AddMonoidHom.instFunLike` `embedProduct`	—	`continuous_induced_dom`
`continuous_iff` 📖	mathematical	—	`Continuous` `AddUnits` `instTopologicalSpaceAddUnits` `val` `instNeg`	—	`Topology.IsInducing.continuous_iff` `isInducing_embedProduct` `continuous_prodMk` `Homeomorph.isInducing`
`continuous_map` 📖	mathematical	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddUnits` `instTopologicalSpaceAddUnits` `instAddZeroClass` `map`	—	`continuous_iff` `Continuous.comp` `continuous_val` `continuous_coe_neg`
`continuous_val` 📖	mathematical	—	`Continuous` `AddUnits` `instTopologicalSpaceAddUnits` `val`	—	`Continuous.fst` `continuous_embedProduct`
`embedding_val_mk` 📖	mathematical	`ContinuousOn` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `setOf` `IsAddUnit` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`Topology.IsEmbedding` `AddUnits` `instTopologicalSpaceAddUnits` `val`	—	`isEmbedding_val_mk'` `val_neg_eq_neg_val`
`instDiscreteTopology` 📖	mathematical	—	`DiscreteTopology` `AddUnits` `instTopologicalSpaceAddUnits`	—	`Topology.IsEmbedding.discreteTopology` `instDiscreteTopologyProd` `AddOpposite.instDiscreteTopology` `isEmbedding_embedProduct`
`instT2Space` 📖	mathematical	—	`T2Space` `AddUnits` `instTopologicalSpaceAddUnits`	—	`Topology.IsEmbedding.t2Space` `Prod.t2Space` `AddOpposite.instT2Space` `isEmbedding_embedProduct`
`isEmbedding_embedProduct` 📖	mathematical	—	`Topology.IsEmbedding` `AddUnits` `AddOpposite` `instTopologicalSpaceAddUnits` `instTopologicalSpaceProd` `AddOpposite.instTopologicalSpaceAddOpposite` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddOpposite.instAddZeroClass` `AddMonoidHom.instFunLike` `embedProduct`	—	`isInducing_embedProduct` `embedProduct_injective`
`isEmbedding_val_mk'` 📖	mathematical	`ContinuousOn` `setOf` `IsAddUnit` `val` `AddUnits` `instNeg`	`Topology.IsEmbedding` `instTopologicalSpaceAddUnits`	—	`topology_eq_inf` `inf_eq_left` `continuous_iff_le_induced` `continuous_iff_continuousAt` `nhds_induced` `Filter.mem_map` `Filter.mem_inf_principal` `isAddUnit` `val_injective`
`isInducing_embedProduct` 📖	mathematical	—	`Topology.IsInducing` `AddUnits` `AddOpposite` `instTopologicalSpaceAddUnits` `instTopologicalSpaceProd` `AddOpposite.instTopologicalSpaceAddOpposite` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddOpposite.instAddZeroClass` `AddMonoidHom.instFunLike` `embedProduct`	—	—
`isOpenMap_map` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `IsOpenMap`	`AddUnits` `instTopologicalSpaceAddUnits` `instAddZeroClass` `map`	—	`IsOpenMap.prodMap` `IsOpenMap.comp` `Homeomorph.isOpenMap` `Set.ext` `Set.image_congr` `Set.mem_preimage` `Set.mem_image` `AddOpposite.exists` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `add_neg` `map_zero` `AddMonoidHomClass.toZeroHomClass` `neg_add` `mk_val`
`topology_eq_inf` 📖	mathematical	—	`instTopologicalSpaceAddUnits` `TopologicalSpace` `AddUnits` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.induced` `val` `instNeg`	—	`Topology.IsInducing.eq_induced` `isInducing_embedProduct` `induced_compose` `induced_inf`

MulOpposite

Definitions

Name	Category	Theorems
`instTopologicalSpaceMulOpposite` 📖	CompOp	48 math math: `continuousConstSMul`, `map_op_nhds`, `instContinuousMul`, `FormalMultilinearSeries.ofScalarsSum_op`, `summable_unop`, `comap_unop_nhds`, `instLocallyCompactSpace`, `opContinuousLinearEquiv_symm_apply`, `NormedSpace.exp_op`, `hasSum_unop`, `instIsTopologicalGroupMulOpposite`, `continuous_unop`, `instIsTopologicalRingMulOpposite`, `Units.isEmbedding_embedProduct`, `instContinuousAddMulOpposite`, `instContinuousNegMulOpposite`, `ContinuousSMul.op`, `IsTopologicalSemiring.toOppositeIsModuleTopology`, `HasSum.op`, `hasSum_op`, `tsum_unop`, `comap_op_leftUniformSpace`, `instDiscreteTopology`, `continuousSMul`, `Units.isClosedEmbedding_embedProduct`, `map_unop_nhds`, `opHomeomorph_symm_apply`, `comap_op_nhds`, `instWeaklyLocallyCompactSpace`, `instContinuousInvMulOpposite`, `instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe`, `Units.continuous_embedProduct`, `instProperSMulMulOppositeOfIsTopologicalGroup`, `instIsTopologicalSemiringMulOpposite`, `summable_op`, `opContinuousLinearEquiv_apply`, `comap_op_rightUniformSpace`, `instCompactSpace`, `continuous_op`, `tsum_op`, `Units.isInducing_embedProduct`, `instContinuousStarMulOpposite`, `NormedSpace.exp_unop`, `ContinuousMul.to_continuousSMul_op`, `opHomeomorph_apply`, `FormalMultilinearSeries.ofScalarsSum_unop`, `instT2Space`, `Summable.op`
`opHomeomorph` 📖	CompOp	2 math math: `opHomeomorph_symm_apply`, `opHomeomorph_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_op_nhds` 📖	mathematical	—	`Filter.comap` `MulOpposite` `op` `nhds` `instTopologicalSpaceMulOpposite` `unop`	—	`Homeomorph.comap_nhds_eq`
`comap_unop_nhds` 📖	mathematical	—	`Filter.comap` `MulOpposite` `unop` `nhds` `instTopologicalSpaceMulOpposite` `op`	—	`Homeomorph.comap_nhds_eq`
`continuous_op` 📖	mathematical	—	`Continuous` `MulOpposite` `instTopologicalSpaceMulOpposite` `op`	—	`continuous_induced_rng` `continuous_id`
`continuous_unop` 📖	mathematical	—	`Continuous` `MulOpposite` `instTopologicalSpaceMulOpposite` `unop`	—	`continuous_induced_dom`
`instCompactSpace` 📖	mathematical	—	`CompactSpace` `MulOpposite` `instTopologicalSpaceMulOpposite`	—	`Homeomorph.compactSpace`
`instDiscreteTopology` 📖	mathematical	—	`DiscreteTopology` `MulOpposite` `instTopologicalSpaceMulOpposite`	—	`Topology.IsEmbedding.discreteTopology` `Homeomorph.isEmbedding`
`instLocallyCompactSpace` 📖	mathematical	—	`LocallyCompactSpace` `MulOpposite` `instTopologicalSpaceMulOpposite`	—	`Topology.IsClosedEmbedding.locallyCompactSpace` `Homeomorph.isClosedEmbedding`
`instT2Space` 📖	mathematical	—	`T2Space` `MulOpposite` `instTopologicalSpaceMulOpposite`	—	`Homeomorph.t2Space`
`instWeaklyLocallyCompactSpace` 📖	mathematical	—	`WeaklyLocallyCompactSpace` `MulOpposite` `instTopologicalSpaceMulOpposite`	—	`Topology.IsClosedEmbedding.weaklyLocallyCompactSpace` `Homeomorph.isClosedEmbedding`
`map_op_nhds` 📖	mathematical	—	`Filter.map` `MulOpposite` `op` `nhds` `instTopologicalSpaceMulOpposite`	—	`Homeomorph.map_nhds_eq`
`map_unop_nhds` 📖	mathematical	—	`Filter.map` `MulOpposite` `unop` `nhds` `instTopologicalSpaceMulOpposite`	—	`Homeomorph.map_nhds_eq`
`opHomeomorph_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `MulOpposite` `instTopologicalSpaceMulOpposite` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `opHomeomorph` `op`	—	—
`opHomeomorph_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `MulOpposite` `instTopologicalSpaceMulOpposite` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `opHomeomorph` `unop`	—	—

Units

Definitions

Name	Category	Theorems
`instTopologicalSpaceUnits` 📖	CompOp	66 math math: `Matrix.SpecialLinearGroup.continuous_toGL`, `Complex.isQuotientCoveringMap_npow`, `ContinuousMap.val_unitsLift_apply_apply`, `Complex.instPathConnectedSpaceUnits`, `Matrix.SpecialLinearGroup.isClosedEmbedding_toGL`, `instCompactSpaceOfT1SpaceOfContinuousMul`, `continuous_val`, `instIsTopologicalGroupOfContinuousMul`, `Matrix.GeneralLinearGroup.continuous_det`, `isEmbedding_val_mk'`, `instDiscreteTopology`, `instIsManifoldModelWithCornersSelf`, `instContinuousMul`, `instLocallyCompactSpaceOfT1SpaceOfContinuousMul`, `isQuotientCoveringMap_npow`, `Nonneg.val_unitsHomeomorphPos_symm_apply_coe`, `ContinuousMap.unitsOfForallIsUnit_apply`, `IsOpenUnits.isOpenEmbedding_unitsVal`, `Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt`, `ContinuousMap.val_unitsLift_symm_apply_apply`, `instLieGroupModelWithCornersSelf`, `Matrix.SpecialLinearGroup.isInducing_mapGL`, `Nonneg.val_inv_unitsHomeomorphPos_symm_apply_coe`, `Submonoid.units_isCompact`, `Matrix.GeneralLinearGroup.continuous_upperRightHom`, `Submonoid.isOpen_units`, `symm_mapContinuousMulEquiv`, `ContinuousMap.unitsLift_apply_inv_apply`, `isEmbedding_embedProduct`, `isOpenMap_map`, `Nonneg.unitsHomeomorphPos_apply_coe`, `instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousMul`, `Matrix.SpecialLinearGroup.isEmbedding_toGL`, `continuous_iff`, `isQuotientCoveringMap_zpow`, `instContinuousStarUnits`, `embedding_val_mk`, `ContinuousMap.continuous_isUnit_unit`, `isEmbedding_val`, `Continuous.of_coeHom_comp`, `topology_eq_inf`, `Continuous.units_map`, `instT2Space`, `isOpenUnits_iff`, `ContinuousMap.canLift`, `toMulEquiv_mapContinuousMulEquiv`, `continuous_coe_inv`, `isClosedEmbedding_embedProduct`, `isEmbedding_val₀`, `continuous_embedProduct`, `continuous_map`, `contMDiff_val`, `Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange`, `ContinuousMap.unitsLift_symm_apply_apply_inv'`, `continuousSMul`, `isOpenEmbedding_val`, `chartAt_source`, `Matrix.SpecialLinearGroup.isInducing_toGL`, `isOpenMap_val`, `isInducing_embedProduct`, `mapContinuousMulEquiv_apply`, `Subgroup.IsArithmetic.discreteTopology`, `cyclotomicCharacter.continuous`, `instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space`, `Matrix.SpecialLinearGroup.isEmbedding_mapGL`, `chartAt_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_coe_inv` 📖	mathematical	—	`Continuous` `Units` `instTopologicalSpaceUnits` `val` `instInv`	—	`continuous_iff` `continuous_id`
`continuous_embedProduct` 📖	mathematical	—	`Continuous` `Units` `MulOpposite` `instTopologicalSpaceUnits` `instTopologicalSpaceProd` `MulOpposite.instTopologicalSpaceMulOpposite` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instMulOneClass` `Prod.instMulOneClass` `Monoid.toMulOneClass` `MulOpposite.instMulOneClass` `MonoidHom.instFunLike` `embedProduct`	—	`continuous_induced_dom`
`continuous_iff` 📖	mathematical	—	`Continuous` `Units` `instTopologicalSpaceUnits` `val` `instInv`	—	`Topology.IsInducing.continuous_iff` `isInducing_embedProduct` `Homeomorph.isInducing`
`continuous_map` 📖	mathematical	`Continuous` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`Units` `instTopologicalSpaceUnits` `instMulOneClass` `map`	—	`continuous_iff` `Continuous.comp` `continuous_val` `continuous_coe_inv`
`continuous_val` 📖	mathematical	—	`Continuous` `Units` `instTopologicalSpaceUnits` `val`	—	`Continuous.fst` `continuous_embedProduct`
`embedding_val_mk` 📖	mathematical	`ContinuousOn` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `setOf` `IsUnit` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`Topology.IsEmbedding` `Units` `instTopologicalSpaceUnits` `val`	—	`isEmbedding_val_mk'` `val_inv_eq_inv_val`
`instDiscreteTopology` 📖	mathematical	—	`DiscreteTopology` `Units` `instTopologicalSpaceUnits`	—	`Topology.IsEmbedding.discreteTopology` `instDiscreteTopologyProd` `MulOpposite.instDiscreteTopology` `isEmbedding_embedProduct`
`instT2Space` 📖	mathematical	—	`T2Space` `Units` `instTopologicalSpaceUnits`	—	`Topology.IsEmbedding.t2Space` `Prod.t2Space` `MulOpposite.instT2Space` `isEmbedding_embedProduct`
`isEmbedding_embedProduct` 📖	mathematical	—	`Topology.IsEmbedding` `Units` `MulOpposite` `instTopologicalSpaceUnits` `instTopologicalSpaceProd` `MulOpposite.instTopologicalSpaceMulOpposite` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instMulOneClass` `Prod.instMulOneClass` `Monoid.toMulOneClass` `MulOpposite.instMulOneClass` `MonoidHom.instFunLike` `embedProduct`	—	`isInducing_embedProduct` `embedProduct_injective`
`isEmbedding_val_mk'` 📖	mathematical	`ContinuousOn` `setOf` `IsUnit` `val` `Units` `instInv`	`Topology.IsEmbedding` `instTopologicalSpaceUnits`	—	`topology_eq_inf` `inf_eq_left` `continuous_iff_le_induced` `continuous_iff_continuousAt` `nhds_induced` `Filter.mem_inf_principal` `isUnit` `val_injective`
`isInducing_embedProduct` 📖	mathematical	—	`Topology.IsInducing` `Units` `MulOpposite` `instTopologicalSpaceUnits` `instTopologicalSpaceProd` `MulOpposite.instTopologicalSpaceMulOpposite` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instMulOneClass` `Prod.instMulOneClass` `Monoid.toMulOneClass` `MulOpposite.instMulOneClass` `MonoidHom.instFunLike` `embedProduct`	—	—
`isOpenMap_map` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `IsOpenMap`	`Units` `instTopologicalSpaceUnits` `instMulOneClass` `map`	—	`IsOpenMap.prodMap` `IsOpenMap.comp` `Homeomorph.isOpenMap` `Set.ext` `Set.image_congr` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `mul_inv` `map_one` `MonoidHomClass.toOneHomClass` `inv_mul` `mk_val`
`topology_eq_inf` 📖	mathematical	—	`instTopologicalSpaceUnits` `TopologicalSpace` `Units` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.induced` `val` `instInv`	—	`Topology.IsInducing.eq_induced` `isInducing_embedProduct` `induced_compose` `induced_inf`

---

← Back to Index