instTransForallEventuallyEq — Mathlib

English

The relation of eventual equality along a filter is transitive: if f =^l g and g =^l h, then f =^l h.

Русский

Относительность пограничного равенства по фильтру транзитивна: если f =^l g и g =^l h, то f =^l h.

LaTeX

$$$\\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall f,g,h \\\\in \\\\alpha \\\\to \\\\beta, \\\\bigl(f =^l g \\\\land \\\\ g =^l h\\\\bigr) \\\\Rightarrow \\\\ f =^l h$$$

Lean4

instance {l : Filter α} : Trans ((· =ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· =ᶠ[l] ·) (· =ᶠ[l] ·) where
  trans := EventuallyEq.trans

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