piecewise — Mathlib

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]
Похожие утверждения