For all statement to function

Stream: Is there code for X?

[Timothy Harevy]

Is there a code for if I have

$$\forall n \in \mathbb{N},y*n\le x$$

is there a way I can view a for-all statement as a function of n that is bounded above by x

[Riccardo Brasca]

Can you be a little more precise? Do you want to write in lean this statement?

[Yakov Pechersky]

My guess is the value Sup (Set.range (. * n))

[Timothy Harevy]

I have a statement that says for all n, yn is less than equal to x I want to change that in LEAN to the function yn that is bounded above by x

[Kevin Buzzard]

Can you write the lean code for what you have and what you want, rather than just writing mathematics? There are many lean implementations of one mathematical specification.

[Timothy Harevy]

I have shown this

have h : ∀ (n : ℕ), x ≥ y * n

And want to know of it is possible to change this statement into the form

is_upper_bound (fun n ↦ y*n) x

[Riccardo Brasca]

Can you write a #mwe? is_upper_bound does not exist in mathlib.

[Timothy Harevy]

I've defined it as such

def is_upper_bound {α : Type u} [Preorder α] (A : Set α) (M:α) :=
  ∀x∈A,x≤M

[Riccardo Brasca]

In this case is_upper_bound (fun n ↦ y*n) x does not make sense, since (fun n ↦ y*n) is a function, not a set.

[Riccardo Brasca]

(also note that we have docs#upperBounds)

[Timothy Harevy]

Okay thank you

[Riccardo Brasca]

You can of course consider the upper bound of the range of the function, that is what you want.

[Riccardo Brasca]

import Mathlib

universe u

def is_upper_bound {α : Type u} [Preorder α] (A : Set α) (M:α) :=
  ∀x∈A,x≤M

example (x y : ℕ) (h : ∀ (n : ℕ), x ≥ y * n) :
    is_upper_bound (Set.range fun n ↦ y*n) x := by
  intro a ⟨b, hb⟩
  rw [← hb]
  exact h b

[Riccardo Brasca]

Or

example (x y : ℕ) (h : ∀ (n : ℕ), x ≥ y * n) :
    is_upper_bound (Set.range fun n ↦ y*n) x :=
  fun _ ⟨b, hb⟩ ↦ hb.symm ▸ h b

if you like making things unreadable.

[Yury G. Kudryashov]

We also have docs#Set.forall_range_iff