def C03S03.FnUb (f : ℝ → ℝ) (a : ℝ) : Prop

Equations

• C03S03.FnUb f a = ∀ (x : ℝ), f x ≤ a

def C03S03.FnLb (f : ℝ → ℝ) (a : ℝ) : Prop

Equations

• C03S03.FnLb f a = ∀ (x : ℝ), a ≤ f x

def C03S03.FnHasUb (f : ℝ → ℝ) : Prop

Equations

• C03S03.FnHasUb f = ∃ (a : ℝ), C03S03.FnUb f a

def C03S03.FnHasLb (f : ℝ → ℝ) : Prop

Equations

• C03S03.FnHasLb f = ∃ (a : ℝ), C03S03.FnLb f a