blimsup_sup_not — Mathlib

English

The Not-p and p join to limsup: blimsup u f (¬p ·) ⊔ blimsup u f p = limsup u f.

Русский

СоединениеNot-p и p даёт limsup: blimsup u f (¬p ·) ⊔ blimsup u f p = limsup u f.

LaTeX

$$$\\operatorname{blimsup}(u,f,\\lnot p\\cdot) \\sqcup \\operatorname{blimsup}(u,f,p) = \\operatorname{limsup} u f$$$

Lean4

@[simp]
theorem blimsup_sup_not : blimsup u f p ⊔ blimsup u f (¬p ·) = limsup u f := by
  simp_rw [← blimsup_or_eq_sup, or_not, blimsup_true]

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