exists_of_nonempty_of_not_isPredPrelimit

English

If x is the greatest lower bound of the range of f and x is not a pred-prelimit, then there exists i with f(i) = x.

Русский

Если x является наибольшей нижней гранью множества значений функции f и x не является pred-пределом, тогда существует i, такое что f(i) = x.

LaTeX

$$$ IsGLB (range\\, f)\\, x \\land \\neg IsPredPrelimit x \\Rightarrow \\exists i\\, f(i) = x $$$

Lean4

theorem exists_of_nonempty_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬IsPredPrelimit x) : ∃ i, f i = x :=
  hf.mem_of_nonempty_of_not_isPredPrelimit (range_nonempty f) hx

Похожие утверждения