congr — Mathlib

English

If f and g are eventually equal along l and f(a)=g(a), then IsMinFilter transfers from f to g.

Русский

Если f и g эквивалентны вдоль l и f(a)=g(a), то IsMinFilter переносится на g.

LaTeX

$$$\\mathrm{IsMinFilter}(f,l,a) \\land (f =^l g) \\land (f(a)=g(a)) \\Rightarrow \\mathrm{IsMinFilter}(g,l,a)$$$

Lean4

theorem congr {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (h : IsMinFilter f l a) (heq : f =ᶠ[l] g)
    (hfga : f a = g a) : IsMinFilter g l a :=
  heq.le.isMinFilter hfga h

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