bliminf_or_le_inf_aux_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem bliminf_or_le_inf_aux_left : (bliminf u f fun x => p x ∨ q x) ≤ bliminf u f p :=
  bliminf_or_le_inf.trans inf_le_left

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