EReal.embedding_coe_ennreal
theorem EReal.embedding_coe_ennreal : Embedding ENNReal.toEReal
The theorem `EReal.embedding_coe_ennreal` asserts that the function `ENNReal.toEReal` is an embedding. In other words, it establishes that the function `ENNReal.toEReal`, which maps nonnegative extended real numbers to extended real numbers, is an injection (one-to-one) and preserves the structure of the set, i.e. if two elements in the domain are related, their images in the codomain are also related in the same way. This property plays a crucial role in preserving the mathematical structure when transitioning from the set of nonnegative extended real numbers to the set of extended real numbers.
More concisely: The `ENNReal.toEReal` function is a strict monotonically increasing embedding from non-negative extended real numbers to extended real numbers.
|
EReal.continuousAt_add
theorem EReal.continuousAt_add :
∀ {p : EReal × EReal}, p.1 ≠ ⊤ ∨ p.2 ≠ ⊥ → p.1 ≠ ⊥ ∨ p.2 ≠ ⊤ → ContinuousAt (fun p => p.1 + p.2) p
The theorem `EReal.continuousAt_add` states that the addition operation on `EReal` (which represents the extended real number line, including negative infinity and positive infinity) is continuous at any point, except where it doesn't make sense - specifically at the pair of points (negative infinity, positive infinity) and (positive infinity, negative infinity). This means that if you get closer and closer to any particular point (or pair of points) in `EReal`, the value of the addition operation at those points gets closer and closer to the value at the point you're approaching, unless you're approaching (negative infinity, positive infinity) or (positive infinity, negative infinity).
More concisely: The addition operation on `EReal` is continuous everywhere except at the points (negative infinity, positive infinity) and (positive infinity, negative infinity).
|
EReal.nhds_top_basis
theorem EReal.nhds_top_basis : (nhds ⊤).HasBasis (fun x => True) fun x => Set.Ioi ↑x
This theorem states that the neighborhood filter at positive infinity (`nhds ⊤`) in the extended real numbers (`EReal`) has a basis where each basis element is an interval of the form `(x, ∞)`, where `x` is a real number. In other words, every neighborhood of positive infinity can be generated by taking unions of sets that are open intervals extending to positive infinity from some real number.
More concisely: The neighborhood filter at positive infinity in the extended real numbers has a basis consisting of intervals of the form (x, ∞), where x is a real number.
|
EReal.nhds_bot_basis
theorem EReal.nhds_bot_basis : (nhds ⊥).HasBasis (fun x => True) fun x => Set.Iio ↑x
This theorem states that the neighborhood filter at the bottom element, represented as `⊥` in extended real numbers (`EReal`), has a basis consisting of left-infinite right-open intervals. In other words, the filter of all neighborhoods around negative infinity in the extended real numbers has a basis such that each basis element is a set of real numbers less than some given real number. This basis is represented by the predicate function that always returns true.
More concisely: The neighborhood filter at the bottom element of extended real numbers has a basis consisting of left-infinite right-open intervals.
|
EReal.embedding_coe
theorem EReal.embedding_coe : Embedding Real.toEReal
The theorem `EReal.embedding_coe` states that the function `Real.toEReal`, which maps real numbers to extended real numbers, is an embedding. In other words, it preserves the structure of real numbers when mapping them to the extended real numbers. This means that if two real numbers are distinct, their images under this function in the extended real numbers are also distinct, and the relative order of real numbers is preserved in the extended real numbers.
More concisely: The function `Real.toEReal` is an embedding of the real numbers into the extended real numbers, preserving the order and distinctness of real numbers.
|