Theorems · Theorem · real analysis

leftLim_eq_of_eq_bot

∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [hα : TopologicalSpace α]
  [h'α : OrderTopology α] (f : α → β) {a : α}, nhdsWithin a (Set.Iio a) = ⊥ → Function.leftLim f a = f a

Defined in

Mathlib.Topology.Order.LeftRightLim

Cited by

11 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceTopologicalSpaceOrderTopology