of_forall_eventually_lt_iff — Mathlib

English

If for every x you have f(a) < x iff g(a) < x eventually along l, then f and g are eventually equal along l.

Русский

Если для каждого x выполняется, что асимптотически вдоль l выполняется f(a) < x эквивалентно g(a) < x, то f и g равны в пределе вдоль l.

LaTeX

$$$ (\forall x, \forall^{\infty}_{a \in l} \; f(a) < x \leftrightarrow g(a) < x) \Rightarrow f =^l g $$$

Lean4

theorem of_forall_eventually_lt_iff (h : ∀ x, ∀ᶠ a in l, f a < x ↔ g a < x) : f =ᶠ[l] g :=
  of_forall_separating_preimage (· ∈ range Iio) <| forall_mem_range.2 <| fun x ↦ .set_eq (h x)

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