bliminf_eq_iSup_biInf_of_nat — Mathlib

English

Let p : ℕ → Prop and u : ℕ → α. Then bliminf u atTop p = ⨆ i, ⨅ (j) (_ : p j ∧ i ≤ j), u j.

Русский

Пусть p : ℕ → Prop и u : ℕ → α. Тогда bliminf u atTop p = ⨆ i, ⨅ j (p(j) ∧ i ≤ j), u(j).

LaTeX

$$$\\displaystyle \\operatorname{bliminf} u \\;\\text{atTop} \\;p = \\big\\vee_{i \\in \\mathbb{N}} \\bigl( \\inf_{j:\\, p(j) \\land i \\le j} u(j) \\bigr)$$$

Lean4

theorem bliminf_eq_iSup_biInf_of_nat {p : ℕ → Prop} {u : ℕ → α} :
    bliminf u atTop p = ⨆ i, ⨅ (j) (_ : p j ∧ i ≤ j), u j :=
  @blimsup_eq_iInf_biSup_of_nat αᵒᵈ _ p u

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