piecewise_apply_left — Mathlib

English

If x ∈ C1, then (piecewise h1 h2 h f g hfg) x = f ⟨x, hx⟩.

Русский

Если x ∈ C1, то (piecewise h1 h2 h f g hfg) x = f ⟨x, hx⟩.

LaTeX

$$$(piecewise\\ h_1\\ h_2\\ h\\ f\\ g\\ hfg)\\ x = f\\ ⟨x,\\, hx\\⟩$$$

Lean4

@[simp]
theorem piecewise_apply_left {C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂) (h : C₁ ∪ C₂ = Set.univ)
    (f : LocallyConstant C₁ Z) (g : LocallyConstant C₂ Z)
    (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, hx.1⟩ = g ⟨x, hx.2⟩) [DecidablePred (· ∈ C₁)] (x : X) (hx : x ∈ C₁) :
    piecewise h₁ h₂ h f g hfg x = f ⟨x, hx⟩ :=
  by
  simp only [piecewise, coe_mk]
  rw [dif_pos hx]

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