blimsup_sup_le_or — Mathlib

English

Let α be a complete lattice, f a filter on β, and p, q : β → Prop. Then blimsup u f p ⊔ blimsup u f q ≤ blimsup u f (p ∨ q).

Русский

Пусть α — полная решетка, f — фильтр на β, p, q : β → Prop. Тогда blimsup u f p ⊔ blimsup u f q ≤ blimsup u f (p ∨ q).

LaTeX

$$$\\operatorname{blimsup}(u,f,p) \\;\\sqcup\\; \\operatorname{blimsup}(u,f,q) \\le \\operatorname{blimsup}(u,f,\\lambda x. p(x) \\lor q(x))$$$

Lean4

/-- See also `Filter.blimsup_or_eq_sup`. -/
theorem blimsup_sup_le_or : blimsup u f p ⊔ blimsup u f q ≤ blimsup u f fun x => p x ∨ q x :=
  sup_le (blimsup_mono <| by tauto) (blimsup_mono <| by tauto)

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