English
If for all i ∈ s, f1(i) ∈ Icc(g1(i), g2(i)) and for i ∉ s, f2(i) ∈ Icc(g1(i), g2(i)), then the piecewise function s.piecewise f1 f2 is in Icc g1 g2.
Русский
Если для всех i ∈ s выполнено f1(i) ∈ Icc(g1(i), g2(i)) и для i ∉ s выполнено f2(i) ∈ Icc(g1(i), g2(i)), то функция piecewise принадлежат Icc(g1,g2).
LaTeX
$$$$ s.piecewise\; f_1\; f_2 \in Icc(g_1,g_2) $$$$
Lean4
theorem piecewise_mem_Icc {s : Set ι} [∀ j, Decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : ∀ i, α i}
(h₁ : ∀ i ∈ s, f₁ i ∈ Icc (g₁ i) (g₂ i)) (h₂ : ∀ i ∉ s, f₂ i ∈ Icc (g₁ i) (g₂ i)) : s.piecewise f₁ f₂ ∈ Icc g₁ g₂ :=
⟨le_piecewise (fun i hi ↦ (h₁ i hi).1) fun i hi ↦ (h₂ i hi).1,
piecewise_le (fun i hi ↦ (h₁ i hi).2) fun i hi ↦ (h₂ i hi).2⟩
