bliminf_not_inf

Mathlib.Order.LiminfLimsup

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

English

As above, applying an order isomorphism to bliminf equals bliminf with composed map.

Русский

Аналогично, применение канонической изоморфии к bliminf равно bliminf с композицией.

LaTeX

$$$e\\,(\\operatorname{bliminf} u f p) = \\operatorname{bliminf}(e \\circ u) f p$$$

Lean4

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

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

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

Разделы

Аффилиация

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