bliminf_set_eq — Mathlib

English

For the cofinite filter, bliminf s cofinite p equals the set of x such that {n | p n ∧ x ∉ s n} is Finite.

Русский

Для cofinite bliminf s cofinite p множество x : {n | p n ∧ x ∉ s n} конечно.

LaTeX

$$bliminf s cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}$$

Lean4

theorem bliminf_set_eq : bliminf s cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite} :=
  by
  rw [← compl_inj_iff]
  simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup, cofinite.blimsup_set_eq]
  rfl

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