Theorems · Theorem · real analysis

continuousAt_iff_continuous_left_right

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace β]
  {a : α} {f : α → β}, ContinuousAt f a ↔ ContinuousWithinAt f (Set.Iic a) a ∧ ContinuousWithinAt f (Set.Ici a) a

Defined in

Mathlib.Topology.Order.LeftRight

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderTopologicalSpace