bliminf_sup_le_or_aux_right — Mathlib

English

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

Русский

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

LaTeX

$$$\\operatorname{bliminf}(u,f,q) \\le \\operatorname{bliminf}(u,f,\\lambda x. p(x) \\land q(x))$$$

Lean4

@[simp]
theorem bliminf_sup_le_or_aux_right : blimsup u f q ≤ blimsup u f fun x => p x ∨ q x :=
  le_sup_right.trans blimsup_sup_le_or

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