∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLinearOrder R]
  [inst_1 : TopologicalSpace R] [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S]
  [inst_4 : TopologicalSpace S] [OrderTopology S] {f : R → S},
  Antitone f →
    ∀ (a : ι → R),
      ContinuousAt f (Filter.liminf a F) →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F a) Antitone.map_liminf_of_continuousAt._auto_1 →
          autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F a) Antitone.map_liminf_of_continuousAt._auto_3 →
            f (Filter.liminf a F) = Filter.limsup (f ∘ a) F