liminf_sdiff — Mathlib

English

In a Boolean algebra, removing a fixed element a from liminf equals liminf of pointwise differences: a \\ liminf u f = liminf (λ b. a \\ u b) f.

Русский

В булевой алгебре удаление фиксированного элемента a из лиминфа равно лимину от точечных разностей: a \\ liminf u f = liminf (λ b. a \\ u b) f.

LaTeX

$$$a \\setminus \\liminf u f = \\liminf (\\lambda b. a \\setminus u b) f$$$

Lean4

theorem liminf_sdiff [NeBot f] (a : α) : liminf u f \ a = liminf (fun b => u b \ a) f := by
  simp only [sdiff_eq, inf_comm _ aᶜ, inf_liminf]

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