Complex.UnitDisc.coe_injective
theorem Complex.UnitDisc.coe_injective : Function.Injective Subtype.val
The theorem `Complex.UnitDisc.coe_injective` states that the function `Subtype.val`, when it operates on the subtype corresponding to the complex unit disc, is injective. This implies that for any two elements in the complex unit disc, if they have the same image under `Subtype.val`, then they must be identical. In other words, no two distinct elements of the complex unit disc map to the same point in the codomain.
More concisely: The function `Subtype.val` maps distinct elements in the complex unit disc to distinct values.
|
Complex.UnitDisc.abs_lt_one
theorem Complex.UnitDisc.abs_lt_one : ∀ (z : Complex.UnitDisc), Complex.abs ↑z < 1
This theorem states that for every complex number `z` in the unit disc, the absolute value of `z` is less than one. In other words, the absolute value (or modulus) of any complex number that belongs to the unit disc in the complex plane is strictly less than one. This is consistent with the definition of a unit disc in the complex plane, which includes all complex numbers within a distance less than one from the origin (0,0).
More concisely: For all complex numbers `z`, if `z` is in the unit disc, then the absolute value of `z` is less than 1.
|