Structures · Topology
DiscreteTopology
A topological space is discrete if every set is open, that is,
its topology equals the discrete topology ⊥.
- Defined in
- Mathlib.Topology.Order
- Shape
- One type argument · adds eq_bot
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances39
- Int
- Nat
- Bool
- TopCat.carrier
- ZMod
- Matrix
- DomMulAct
- Units
- DomAddAct
- AddUnits
- PNat
- TopologicalSpace.NonemptyCompacts
- Empty
- Matrix.SpecialLinearGroup
- PEmpty
- AlgEquiv
- PrimeSpectrum
- SignType
- TopologicalSpace.Compacts
- Hamming
- PontryaginDual
- ConnectedComponents
- ZerothHomotopy
- WithDiscreteTopology
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Fin
- PUnit
- AddOpposite
- HasQuotient.Quotient
- Sum
- Multiplicative
- List
- Additive
- Sigma
- Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by350
- isOpen_discrete
- Module.Basis.ofZLatticeBasis
- nhds_discrete
- continuous_of_discreteTopology
- Module.Basis.ofZLatticeBasis_apply
- stabilizer_isOpen
- isClosed_discrete
- BoundedContinuousFunction.extend
- isClopen_discrete
- ZLattice.normBound
- Filter.cocompact_eq_cofinite
- DiscreteTopology.isDiscrete
- ContinuousMap.homeoFnOfDiscrete
- Module.Basis.ofZLatticeBasis_span
- finite_of_compact_of_discrete
- ZLattice.covolume_eq_measure_fundamentalDomain
- Topology.IsEmbedding.discreteTopology
- Subgroup.strictWidthInfty_pos_iff
- MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology
- Homeomorph.discreteTopology
- Metric.isClosedEmbedding_of_pairwise_le_dist
- MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete
- ZLattice.rank
- DiscreteTopology.eq_bot
- ZLattice.covolume_pos
- ContinuousMap.equivFnOfDiscrete
- ZLattice.summable_norm_sub_zpow
- Module.Basis.ofZLatticeBasis_repr_apply
- ZLattice.isAddFundamentalDomain
- ZLattice.normBound_pos
- Topology.IsQuotientMap.trivializationOfSMulDisjoint
- Topology.IsQuotientMap.trivializationOfVAddDisjoint
- AddCircle.openPartialHomeomorphCoe
- ZLattice.summable_norm_rpow
- Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty
- IsCompact.finite_of_discrete
- IsLocallyConstant.iff_continuous
- ZLattice.covolume_eq_det
- IsOpen.trivializationDiscrete
- ZLattice.module_finite
- PrimeSpectrum.toPiLocalizationEquiv
- tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding
- AddEquiv.lpBCF
- ZLattice.volume_image_eq_volume_div_covolume
- ZLattice.tsumNormRPowBound
- Equiv.toHomeomorphOfDiscrete
- continuous_discrete_rng
- IsLocalHomeomorphOn.discreteTopology_of_image
- ZLattice.covolume_comap
- PiNat.metricSpace
Ancestors0
No ancestors.