congr — Mathlib

English

If f is an extrinsic filter and f equals g along l, then g is an extrinsic filter at a.

Русский

Если f является экстр фильтром и совпадает с g вдоль l, то g — экстр фильтр в a.

LaTeX

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

Lean4

theorem congr {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (h : IsExtrFilter f l a) (heq : f =ᶠ[l] g)
    (hfga : f a = g a) : IsExtrFilter g l a := by
  rw [IsExtrFilter] at *
  rwa [← heq.isMaxFilter_iff hfga, ← heq.isMinFilter_iff hfga]

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