bliminf_sup_le_and_aux_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem bliminf_sup_le_and_aux_left : bliminf u f p ≤ bliminf u f fun x => p x ∧ q x :=
  le_sup_left.trans bliminf_sup_le_and

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