IsOpenUnits

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

Statistics

Metric	Count
Definitions IsOpenUnits	1
Theorems isOpenEmbedding_unitsVal, of_isAdic, instIsOpenUnitsOfContinuousInv, instIsOpenUnitsOfContinuousInv₀OfT1Space, instIsOpenUnitsOfDiscreteTopology, isOpenUnits_iff	6
Total	7

IsOpenUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenEmbedding_unitsVal 📖	mathematical	—	Topology.IsOpenEmbedding Units Units.instTopologicalSpaceUnits Units.val	—	—
of_isAdic 📖	mathematical	IsAdic Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring Submodule.instBot	IsOpenUnits MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap Units.continuous_val Units.val_injective IsTopologicalGroup.isOpenMap_iff_nhds_one Units.instIsTopologicalGroupOfContinuousMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass MonoidHom.instMonoidHomClass nhds_induced nhds_prod_eq inv_one IsScalarTower.right Ideal.hasBasis_nhds_adic Filter.HasBasis.prod Filter.HasBasis.comap Set.image_congr Filter.HasBasis.mem_iff' Filter.HasBasis.map Homeomorph.comap_nhds_eq Set.image_add_left Ideal.pow_le_pow_right Ideal.mem_jacobson_bot Ideal.pow_le_self add_comm mul_one neg_add_cancel_left mul_add Distrib.leftDistribClass mul_neg IsUnit.val_inv_mul neg_add_rev neg_add_cancel_right neg_mul Ideal.mul_mem_left

(root)

Definitions

Name	Category	Theorems
IsOpenUnits 📖	CompData	5 math math: instIsOpenUnitsOfContinuousInv₀OfT1Space, instIsOpenUnitsOfContinuousInv, isOpenUnits_iff, instIsOpenUnitsOfDiscreteTopology, IsOpenUnits.of_isAdic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOpenUnitsOfContinuousInv 📖	mathematical	—	IsOpenUnits DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Homeomorph.isOpenEmbedding
instIsOpenUnitsOfContinuousInv₀OfT1Space 📖	mathematical	—	IsOpenUnits MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero	—	Units.isEmbedding_val₀ Set.ext isUnit_iff_ne_zero IsClosed.isOpen_compl isClosed_singleton
instIsOpenUnitsOfDiscreteTopology 📖	mathematical	—	IsOpenUnits	—	Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap Units.continuous_val Units.val_injective isOpen_discrete
isOpenUnits_iff 📖	mathematical	—	IsOpenUnits Topology.IsOpenEmbedding Units Units.instTopologicalSpaceUnits Units.val	—	—

---

← Back to Index