bliminf_congr' — Mathlib

English

If eventually u x ≠ ⊤ implies p x ↔ q x, then bliminf u f p = bliminf u f q.

Русский

Если существует условие, что p x ↔ q x для всех x после некоторого момента, то bliminf совпадают.

LaTeX

$$$\\text{bliminf}(u,f,p) = \\text{bliminf}(u,f,q)$$$

Lean4

theorem bliminf_congr' {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ᶠ x in f, u x ≠ ⊤ → (p x ↔ q x)) :
    bliminf u f p = bliminf u f q :=
  blimsup_congr' (α := αᵒᵈ) h

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