piecewise_apply_right — Mathlib

English

If x ∈ C2, then (piecewise h1 h2 h f g hfg) x = g ⟨x, hx⟩; otherwise, it follows the left rule.

Русский

Если x ∈ C2, то (piecewise h1 h2 h f g hfg) x = g ⟨x, hx⟩; иначе следует левая формула.

LaTeX

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

Lean4

@[simp]
theorem piecewise_apply_right {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 = g ⟨x, hx⟩ :=
  by
  simp only [piecewise, coe_mk]
  split_ifs with h
  · exact hfg x ⟨h, hx⟩
  · rfl

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