liminf_eq_sSup_iUnion_iInter — Mathlib

English

If v has a basis given by p and s, then the liminf of f with respect to v equals the supremum over j of the infimums over i in s(j) of f(i).

Русский

Если у v есть базис, заданный p и s, то liminf f v равен верхней границе по j от нижних пределов по i∈s(j) от f(i).

LaTeX

$$$ \\operatorname{liminf} f v = \\bigvee_{j} \\bigwedge_{i \\in s(j)} f(i) $$$

Lean4

theorem liminf_eq_sSup_iUnion_iInter {ι ι' : Type*} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι}
    (hv : v.HasBasis p s) : liminf f v = sSup (⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i)) :=
  by
  simp_rw [liminf_eq, hv.eventually_iff]
  congr 1
  ext x
  simp only [mem_setOf_eq, iInter_coe_set, mem_iUnion, mem_iInter, mem_Iic, Subtype.exists, exists_prop]

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