Theorems · Theorem · general topology

tendsto_comp_coe_Ioo_atBot

∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a b : X} {α : Type u_2}
  {l : Filter α} {f : X → α},
  a < b →
    autoParam (Order.IsPredPrelimit a) tendsto_comp_coe_Ioo_atBot._auto_1 →
      (Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l)

Defined in

Mathlib.Topology.Order.AtTopBotIxx

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopology