Unitary

Statistics

Metric	Count
Definitions	0
Theorems `instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar`, `instContinuousStarSubtypeMemSubmonoidUnitary`, `instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar`, `isClosed_unitary`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar` 📖	mathematical	—	`ContinuousInv` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instTopologicalSpaceSubtype` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Unitary.instGroupSubtypeMemSubmonoidUnitary`	—	`ContinuousStar.continuous_star` `instContinuousStarSubtypeMemSubmonoidUnitary`
`instContinuousStarSubtypeMemSubmonoidUnitary` 📖	mathematical	—	`ContinuousStar` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instTopologicalSpaceSubtype` `Unitary.instStarSubtypeMemSubmonoidUnitary`	—	`continuous_induced_rng` `Continuous.star` `continuous_subtype_val`
`instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar` 📖	mathematical	—	`IsTopologicalGroup` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `instTopologicalSpaceSubtype` `Unitary.instGroupSubtypeMemSubmonoidUnitary`	—	`Submonoid.continuousMul` `instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar`
`isClosed_unitary` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instSetLike` `unitary`	—	`Set.ext` `IsClosed.preimage` `Continuous.prodMk` `Continuous.fun_mul` `Continuous.star` `continuous_id'` `isClosed_singleton` `instT1SpaceProd`

---