blimsup_not_sup

Mathlib.Order.LiminfLimsup

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

English

As above, functoriality of blimsup under order isomorphisms.

Русский

Аналогично, тождественность блимиcупа при порядок изоморфизмах.

LaTeX

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

Lean4

@[simp]
theorem blimsup_not_sup : blimsup u f (¬p ·) ⊔ blimsup u f p = limsup u f := by
  simpa only [not_not] using blimsup_sup_not (p := (¬p ·))

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

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

Разделы

Аффилиация

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