congr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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