eventuallyLE_congr — Mathlib

English

If f ≈ f' and g ≈ g' along l, then f ≤ᶠ[l] g is equivalent to f' ≤ᶠ[l] g'.

Русский

Если f эквивалентно f' вдоль l и g эквивалентно g' вдоль l, то f ≤ᶠ[l] g эквивалентно f' ≤ᶠ[l] g'.

LaTeX

$$$ (f =ᶠ[l] f') ∧ (g =ᶠ[l] g') \\Rightarrow (f ≤ᶠ[l] g \\iff f' ≤ᶠ[l] g') $$$

Lean4

theorem eventuallyLE_congr {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g' :=
  ⟨fun H => H.congr hf hg, fun H => H.congr hf.symm hg.symm⟩

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