iff_eventuallyEq — Mathlib

English

iff_eventuallyEq: f ≡ g atTop implies GrowsPolynomially f iff GrowsPolynomially g; equivalence under eventual equality.

Русский

iff_eventuallyEq: f ≡ g в бесконечности тогда и только тогда, когда GrowsPolynomially f эквивалентно GrowsPolynomially g.

LaTeX

$$f =ᶠ[atTop] g → (GrowsPolynomially f) ↔ (GrowsPolynomially g)$$

Lean4

theorem iff_eventuallyEq {f g : ℝ → ℝ} (h : f =ᶠ[atTop] g) : GrowsPolynomially f ↔ GrowsPolynomially g :=
  ⟨fun hf => congr_of_eventuallyEq h.symm hf, fun hg => congr_of_eventuallyEq h hg⟩

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