congr_left

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsEquivalent.congr_left

← MathLib Explorer

English

Same as 41396: left-congruence property of asymptotic equivalence.

Русский

Свойство слева по конгруэнции асимптотической эквивалентности.

LaTeX

$$huv.congr_left hvw$$

Lean4

theorem congr_left {u v w : α → β} {l : Filter α} (huv : u ~[l] v) (huw : u =ᶠ[l] w) : w ~[l] v :=
  huv.congr' (huw.sub (EventuallyEq.refl _ _)) (EventuallyEq.refl _ _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru