English
For the cofinite filter, blimsup s cofinite p equals the set of x such that {n | p n ∧ x ∈ s n} is Infinite.
Русский
Для фильтра когерентности (cofinite) blimsup s cofinite p равен множеству x таких, что множество {n | p n ∧ x ∈ s n} бесконечно.
LaTeX
$$blimsup s cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite}$$
Lean4
theorem blimsup_set_eq : blimsup s cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite} :=
by
simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]
ext x
refine ⟨fun h => ?_, fun hx t h => ?_⟩ <;> contrapose! h
· simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]
exact ⟨{ x }ᶜ, by simpa using h, by simp⟩
· exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩
