inf_liminf — Mathlib

English

In a distributive lattice with NeBot f, a ⊓ liminf u f = liminf (λ x, a ⊓ u x) f.

Русский

В распределенной решетке с NeBot f выполняется a ⊓ liminf u f = liminf (λ x, a ⊓ u x) f.

LaTeX

$$$\\operatorname{inf}(a, \\operatorname{liminf} u f) = \\operatorname{liminf}(\\lambda x. a \\sqcup u x) f$$$

Lean4

theorem inf_liminf [NeBot f] (a : α) : a ⊓ liminf u f = liminf (fun x => a ⊓ u x) f :=
  sup_limsup (α := αᵒᵈ) a

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