bliminf_inf_not

Mathlib.Order.LiminfLimsup

URI: https://scilib.ai/kg/mathlib#Filter.bliminf_inf_not

English

The inf with not p and p equals liminf: bliminf u f p ⊓ bliminf u f (¬p ·) = liminf u f.

Русский

Инфинф с Not-p и p равно liminf: bliminf u f p ∧ bliminf u f (¬p ·) = liminf u f.

LaTeX

$$$\\operatorname{bliminf}(u,f,p) \\sqcap \\operatorname{bliminf}(u,f,\\lnot p \\cdot) = \\operatorname{liminf} u f$$$

Lean4

@[simp]
theorem bliminf_inf_not : bliminf u f p ⊓ bliminf u f (¬p ·) = liminf u f :=
  blimsup_sup_not (α := αᵒᵈ)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru