Results about division in extended non-negative reals #
This file establishes basic properties related to the inversion and division operations on ℝ≥0∞
.
For instance, as a consequence of being a DivInvOneMonoid
, ℝ≥0∞
inherits a power operation
with integer exponent.
Main results #
A few order isomorphisms are worthy of mention:
OrderIso.invENNReal : ℝ≥0∞ ≃o ℝ≥0∞ᵒᵈ
: The mapx ↦ x⁻¹
as an order isomorphism to the dual.orderIsoIicOneBirational : ℝ≥0∞ ≃o Iic (1 : ℝ≥0∞)
: The birational order isomorphism betweenℝ≥0∞
and the unit intervalSet.Iic (1 : ℝ≥0∞)
given byx ↦ (x⁻¹ + 1)⁻¹
with inversex ↦ (x⁻¹ - 1)⁻¹
orderIsoIicCoe (a : ℝ≥0) : Iic (a : ℝ≥0∞) ≃o Iic a
: Order isomorphism between an initial interval inℝ≥0∞
and an initial interval inℝ≥0
given by the identity map.orderIsoUnitIntervalBirational : ℝ≥0∞ ≃o Icc (0 : ℝ) 1
: An order isomorphism between the extended nonnegative real numbers and the unit interval. This isorderIsoIicOneBirational
composed with the identity order isomorphism betweenIic (1 : ℝ≥0∞)
andIcc (0 : ℝ) 1
.
Alias of the reverse direction of ENNReal.inv_ne_top
.
The inverse map fun x ↦ x⁻¹
is an order isomorphism between ℝ≥0∞
and its OrderDual
Equations
- OrderIso.invENNReal = { toEquiv := Equiv.trans (Equiv.inv ENNReal) OrderDual.toDual, map_rel_iff' := ⋯ }
Instances For
Order isomorphism between an initial interval in ℝ≥0∞
and an initial interval in ℝ≥0
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An order isomorphism between the extended nonnegative real numbers and the unit interval.
Equations
Instances For
Alias of ENNReal.iSup_zero
.
Left multiplication by a nonzero finite a
as an order isomorphism.
Equations
- a.mulLeftOrderIso ha = { toEquiv := ha.unit.mulLeft, map_rel_iff' := ⋯ }
Instances For
Right multiplication by a nonzero finite a
as an order isomorphism.
Equations
- a.mulRightOrderIso ha = { toEquiv := ha.unit.mulRight, map_rel_iff' := ⋯ }
Instances For
Very general version for distributivity of multiplication over an infimum.
See ENNReal.mul_iInf_of_ne
for the special case assuming a ≠ 0
and a ≠ ∞
, and
ENNReal.mul_iInf
for the special case assuming Nonempty ι
.
Very general version for distributivity of multiplication over an infimum.
See ENNReal.iInf_mul_of_ne
for the special case assuming a ≠ 0
and a ≠ ∞
, and
ENNReal.iInf_mul
for the special case assuming Nonempty ι
.
If a ≠ 0
and a ≠ ∞
, then right multiplication by a
maps infimum to infimum.
See ENNReal.mul_iInf'
for the general case, and ENNReal.iInf_mul
for another special case that
assumes Nonempty ι
but does not require a ≠ 0
, and ENNReal
.
If a ≠ 0
and a ≠ ∞
, then right multiplication by a
maps infimum to infimum.
See ENNReal.iInf_mul'
for the general case, and ENNReal.iInf_mul
for another special case that
assumes Nonempty ι
but does not require a ≠ 0
.
See ENNReal.mul_iInf'
for the general case, and ENNReal.mul_iInf_of_ne
for another special
case that assumes a ≠ 0
but does not require Nonempty ι
.
See ENNReal.iInf_mul'
for the general case, and ENNReal.iInf_mul_of_ne
for another special
case that assumes a ≠ 0
but does not require Nonempty ι
.
Very general version for distributivity of division over an infimum.
See ENNReal.iInf_div_of_ne
for the special case assuming a ≠ 0
and a ≠ ∞
, and
ENNReal.iInf_div
for the special case assuming Nonempty ι
.
If a ≠ 0
and a ≠ ∞
, then division by a
maps infimum to infimum.
See ENNReal.iInf_div'
for the general case, and ENNReal.iInf_div
for another special case that
assumes Nonempty ι
but does not require a ≠ ∞
.
See ENNReal.iInf_div'
for the general case, and ENNReal.iInf_div_of_ne
for another special
case that assumes a ≠ ∞
but does not require Nonempty ι
.