monotone function of iInf of antitone function

Stream: Is there code for X?

[Ira Fesefeldt]

I have something similar to this:

import Mathlib

variable (a : α) (b : ℕ → ℤ → α) (f : (ℤ → α) → α)
variable [CompleteLinearOrder α]

example (h_f_mono : Monotone f) (h_b_antitone : Antitone b) (h : ∀ i : ℕ, a ≤ f (fun z => b i z)) :
    a ≤ f (fun z => ⨅ i, b i z) := by
  sorry

Graphically this theorem looks correct to me, but I am not sure how to proof it in Lean and couldn't find any matching theorems...

[Daniel Weber]

I don't think this is true — f could be a jump function, which is 0 at the infimum and 1 at any greater value. I think this is true for continuous f, though

[Ira Fesefeldt]

Fair enough :/