congr_right — Mathlib

English

Let l be a filter on α and f, g, h: α → β. If g and h are eventually equal along l, then f is eventually equal to g if and only if f is eventually equal to h.

Русский

Пусть l — фильтр на α, а f, g, h : α → β. Если g и h тождественны на многоточии вдоль l, то f тождественен g вдоль l тогда и только тогда, когда f тождественен h вдоль l.

LaTeX

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

Lean4

theorem congr_right {l : Filter α} {f g h : α → β} (H : g =ᶠ[l] h) : f =ᶠ[l] g ↔ f =ᶠ[l] h :=
  ⟨(·.trans H), (·.trans H.symm)⟩

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