piecewise_piecewise_of_subset_right

English

If t ⊆ s, then s.piecewise f (t.piecewise g1 g2) = s.piecewise f g2.

Русский

Если t ⊆ s, то s.piecewise f (t.piecewise g1 g2) = s.piecewise f g2.

LaTeX

$$$t \\subseteq s \\Rightarrow s.\\text{piecewise} f (t.\\text{piecewise} g_1 g_2) = s.\\text{piecewise} f g_2.$$$

Lean4

theorem piecewise_piecewise_of_subset_right {s t : Finset ι} [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ t)]
    (h : t ⊆ s) (f g₁ g₂ : ∀ a, π a) : s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂ :=
  s.piecewise_congr (fun _ _ => rfl) fun _i hi => t.piecewise_eq_of_notMem _ _ (mt (@h _) hi)

Похожие утверждения