Lean4
/-- Combine finitely supported functions over `{a // P a}` and `{a // ¬P a}`, by case-splitting on
`P a`. -/
@[simps]
def piecewise (f : Subtype P →₀ M) (g : { a // ¬P a } →₀ M) : α →₀ M
where
toFun a := if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩
support :=
(f.support.map (.subtype _)).disjUnion (g.support.map (.subtype _)) <|
by
simp_rw [Finset.disjoint_left, mem_map, forall_exists_index, Embedding.coe_subtype, Subtype.forall,
Subtype.exists]
rintro _ a ha ⟨-, rfl⟩ ⟨b, hb, -, rfl⟩
exact hb ha
mem_support_toFun a := by by_cases ha : P a <;> simp [ha]