transEventuallyEqIsEquivalent — Mathlib

English

There is a transitive connection between EventuallyEq and IsEquivalent: if f ~_l' g1 and g1 ~_l g2, then f ~_l g2.

Русский

Существует транзитивная связь между EventuallyEq и IsEquivalent: если f =ᶠ[l'] g1 и g1 ~_l g2, то f ~_l g2.

LaTeX

$$f =^\!{l'} g_1 \; \land \; g_1 ~_l g_2 \Rightarrow f ~_l g_2$$

Lean4

instance transEventuallyEqIsEquivalent :
    @Trans (α → β) (α → β) (α → β) (EventuallyEq l) (IsEquivalent l) (IsEquivalent l) where
  trans := EventuallyEq.trans_isEquivalent

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