Theorems · Theorem · general topology

IsExtrFilter.congr

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  IsExtrFilter f l a → f =ᶠ[l] g → f a = g a → IsExtrFilter g l a

Defined in

Mathlib.Order.Filter.Extr

Cited by

5 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

Preorder