English
Let (S_i) be a decreasing family of subsets of a set X, and let f,g be functions from X to a family of sets indexed by X. For any a in X, the value of the piecewise construction with respect to S_i at a eventually equals the piecewise construction with respect to the intersection ⋂_i S_i at a.
Русский
Пусть (S_i) — убывающее семейство подмножеств множества X, а f,g — функции X → соответствующих множеств. Для каждого a в X значения кусочно-задаваемых функций по S_i в точке a сходятся к значению кусочно-задаваемой функции по пересечению ⋂_i S_i в a.
LaTeX
$$$\forall a\in X:\quad \forall^\infty i\ in atTop:\ (S_i)\text{.piecewise } f g a = (\bigcap_i S_i)\text{.piecewise } f g a$$$
Lean4
theorem piecewise_eventually_eq_iInter {β : α → Type*} [Preorder ι] {s : ι → Set α} [∀ i, DecidablePred (· ∈ s i)]
[DecidablePred (· ∈ ⋂ i, s i)] (hs : Antitone s) (f g : (a : α) → β a) (a : α) :
∀ᶠ i in atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a := by
classical
convert ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
· convert congr_fun (Set.piecewise_compl (s _) g f) a
· simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]
