English
If a is a top element, then atTop equals the principal filter on Ici(a).
Русский
Если a является верхним элементом, то atTop равен принципиальному фильтру на Ici(a).
LaTeX
$$$\\text{IsTop}(a) \\Rightarrow \\mathrm{atTop} = \\mathrm{principal}(\\mathrm{Ici}(a)).$$$
Lean4
theorem piecewise_eventually_eq_iUnion {β : α → Type*} [Preorder ι] {s : ι → Set α} [∀ i, DecidablePred (· ∈ s i)]
[DecidablePred (· ∈ ⋃ i, s i)] (hs : Monotone s) (f g : (a : α) → β a) (a : α) :
∀ᶠ i in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a :=
by
rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha
· refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]
· filter_upwards with i
simp only [Set.piecewise_eq_of_notMem, not_exists.1 ha i, mt mem_iUnion.1 ha, not_false_eq_true]
