English
If f1 and f2 both belong to Icc(g1,g2), then s.piecewise f1 f2 belongs to Icc g1 g2.
Русский
Если f1 и f2 принадлежат Icc(g1,g2), то s.piecewise f1 f2 принадлежит 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₁ : f₁ ∈ Icc g₁ g₂)
(h₂ : f₂ ∈ Icc g₁ g₂) : s.piecewise f₁ f₂ ∈ Icc g₁ g₂ :=
piecewise_mem_Icc (fun _ _ ↦ ⟨h₁.1 _, h₁.2 _⟩) fun _ _ ↦ ⟨h₂.1 _, h₂.2 _⟩