bliminf_or_le_inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- See also `Filter.bliminf_or_eq_inf`. -/
theorem bliminf_or_le_inf : (bliminf u f fun x => p x ∨ q x) ≤ bliminf u f p ⊓ bliminf u f q :=
  blimsup_sup_le_or (α := αᵒᵈ)

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