English
The eventuality of nested eventual statements collapses to a single eventual statement on the infimum filter.
Русский
Сходимость вложенных утверждений сводится к единственному утверждению на инфиминном фильтре.
LaTeX
$$$ [@[simp]] \\text{theorem eventually_smallSets_eventually } {p : \\alpha \\to Prop} :\\n (\\\\forall^\\\\infty s \\\\in l.smallSets, \\\\operatorname{Eventually} (fun x => p x) l') \\\\iff \\\\operatorname{Ever}^? (p) $$$
Lean4
@[simp]
theorem eventually_smallSets_eventually {p : α → Prop} :
(∀ᶠ s in l.smallSets, ∀ᶠ x in l', x ∈ s → p x) ↔ ∀ᶠ x in l ⊓ l', p x :=
calc
_ ↔ ∃ s ∈ l, ∀ᶠ x in l', x ∈ s → p x := eventually_smallSets' fun _ _ hst ht => ht.mono fun _ hx hs => hx (hst hs)
_ ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x, x ∈ t → x ∈ s → p x := by simp only [eventually_iff_exists_mem]
_ ↔ ∀ᶠ x in l ⊓ l', p x := by simp only [eventually_inf, and_comm, mem_inter_iff, ← and_imp]
