blimsup_or_eq_sup — Mathlib

English

For α a complete distributive lattice, blimsup u f (p ∨ q) equals the join of blimsup u f p and blimsup u f q.

Русский

Для α—полной распределимой решетки, blimsup u f (p ∨ q) равно объединению blimsup u f p и blimsup u f q.

LaTeX

$$$\\operatorname{blimsup}(u,f, p \\lor q) = \\operatorname{blimsup}(u,f,p) \\sqcup \\operatorname{blimsup}(u,f,q)$$$

Lean4

@[simp]
theorem blimsup_or_eq_sup : (blimsup u f fun x => p x ∨ q x) = blimsup u f p ⊔ blimsup u f q := by
  simp only [blimsup_eq_limsup, ← limsup_sup_filter, ← inf_sup_left, sup_principal, setOf_or]

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