exists_pos — Mathlib

English

If f = OWith c l f g' for some c, then there exists a real number c' > 0 such that f = OWith c' l f g'.

Русский

Если f = OWith c l f g', то существует c' > 0 с таким свойством, что f = OWith c' l f g'.

LaTeX

$$$ IsBigOWith c\ l\ f\ g' \rightarrow \exists c'>0, IsBigOWith c' l f g' $$$

Lean4

theorem exists_pos (h : IsBigOWith c l f g') : ∃ c' > 0, IsBigOWith c' l f g' :=
  ⟨max c 1, lt_of_lt_of_le zero_lt_one (le_max_right c 1), h.weaken <| le_max_left c 1⟩

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