Theorems · Theorem · general topology

EReal.continuousAt_add

∀ {p : EReal × EReal}, p.1 ≠ ⊤ ∨ p.2 ≠ ⊥ → p.1 ≠ ⊥ ∨ p.2 ≠ ⊤ → ContinuousAt (fun p => p.1 + p.2) p

The addition on EReal is continuous except where it doesn't make sense (i.e., at (⊥, ⊤) and at (⊤, ⊥)).

Defined in

Mathlib.Topology.Instances.EReal.Lemmas

Cited by

2 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound