blimsup_congr' — Mathlib

English

If eventually u x ≠ ⊥ implies p x ↔ q x, then blimsup u f p = blimsup u f q.

Русский

Если из некоторой предельной области следует, что p x ↔ q x, тогда blimsup u f p = blimsup u f q.

LaTeX

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

Lean4

theorem blimsup_congr' {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ᶠ x in f, u x ≠ ⊥ → (p x ↔ q x)) :
    blimsup u f p = blimsup u f q := by
  simp only [blimsup_eq]
  congr with a
  refine eventually_congr (h.mono fun b hb => ?_)
  rcases eq_or_ne (u b) ⊥ with hu | hu; · simp [hu]
  rw [hb hu]

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