Structures · Topology
ContinuousInv₀
A type with 0 and Inv such that fun x ↦ x⁻¹ is continuous at all nonzero points. Any
normed (semi)field has this property.
- Defined in
- Mathlib.Topology.Algebra.GroupWithZero
- Shape
- One type argument · adds continuousAt_inv₀
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- NNReal
- NNRat
How is a type an instance?
Loading the hierarchy index…
Assumed by78
- Filter.Tendsto.div
- Filter.Tendsto.inv₀
- ContinuousOn.inv₀
- ContinuousOn.div
- continuousOn_inv₀
- ContinuousOn.fun_inv₀
- Continuous.inv₀
- ContinuousAt.div₀
- ContinuousAt.div
- cfcUnits
- ContinuousInv₀.continuousAt_inv₀
- ContinuousAt.inv₀
- cfc_inv_id
- Filter.tendsto_mul_iff_of_ne_zero
- Continuous.div
- Units.continuousOn_inv₀_spectrum
- Filter.Tendsto.zpow₀
- ContinuousWithinAt.div
- Nonneg.unitsHomeomorphPos
- continuousAt_zpow₀
- HasProd.inv₀
- ContinuousOn.zpow₀
- cfc_inv
- Continuous.div₀
- ContinuousWithinAt.inv₀
- tendsto_natCast_div_add_atTop
- ContinuousOn.div₀
- tendsto_inv₀
- tendsto_inv_iff₀
- continuousOn_zpow₀
- MeasureTheory.AEStronglyMeasurable.inv₀
- val_cfcUnits
- HasProd.div₀
- ContinuousAt.fun_inv₀
- Homeomorph.inv₀
- cfc_zpow
- cfcUnits.congr_simp
- MeasureTheory.StronglyMeasurable.inv₀
- IsPreconnected.eq_of_sq_eq
- MeasureTheory.AEStronglyMeasurable.fun_inv₀
- nhds_inv₀
- tendsto_div_nhds_one_iff_eq₀
- MeasureTheory.StronglyMeasurable.div
- cfcUnits_pow
- val_inv_cfcUnits
- Continuous.zpow₀
- unitsHomeomorphNeZero
- Units.continuousOn_zpow₀_spectrum
- ContinuousWithinAt.zpow₀
- ContinuousAt.comp_div_cases
Ancestors0
No ancestors.