congr_right

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

English

Right-congruence counterpart: if u ~[l] v and v ~[l] w then u ~[l] w.

Русский

Справедливость по правой конгруэнции: если u ~ v и v ~ w, тогда u ~ w.

LaTeX

$$huv ∧ hvw ⇒ huv.trans hvw$$

Lean4

theorem congr_right {u v w : α → β} {l : Filter α} (huv : u ~[l] v) (hvw : v =ᶠ[l] w) : u ~[l] w :=
  (huv.symm.congr_left hvw).symm

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

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

Разделы

Аффилиация

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