English
If p(a) holds, IsRatStieltjesPoint f a; otherwise IsRatStieltjesPoint g a, then IsRatStieltjesPoint of the piecewise function holds at a.
Русский
Если p(a) верно, то IsRatStieltjesPoint f a; иначе IsRatStieltjesPoint g a; тогда для функции if p a then f a else g a выполняется.
LaTeX
$$$IsRatStieltjesPoint\\left( a \\mapsto \\begin{cases} f(a) & p(a) \\\\ g(a) & \\neg p(a) \\end{cases} \\right) a$ при заданных условиях$$
Lean4
theorem ite {f g : α → ℚ → ℝ} {a : α} (p : α → Prop) [DecidablePred p] (hf : p a → IsRatStieltjesPoint f a)
(hg : ¬p a → IsRatStieltjesPoint g a) : IsRatStieltjesPoint (fun a ↦ if p a then f a else g a) a
where
mono := by split_ifs with h; exacts [(hf h).mono, (hg h).mono]
tendsto_atTop_one := by split_ifs with h; exacts [(hf h).tendsto_atTop_one, (hg h).tendsto_atTop_one]
tendsto_atBot_zero := by split_ifs with h; exacts [(hf h).tendsto_atBot_zero, (hg h).tendsto_atBot_zero]
iInf_rat_gt_eq := by split_ifs with h; exacts [(hf h).iInf_rat_gt_eq, (hg h).iInf_rat_gt_eq]
