piecewise_mem_pi — Mathlib

English

If f and g belong to the pi-type pi t t' (i.e., for every index i, f i ∈ t i and g i ∈ t i'), then their piecewise f g also belongs to pi t t'.

Русский

Если f и g относятся к произведению pi t t' (для каждого индекса i, f i ∈ t i и g i ∈ t i'), то s.piecewise f g также относится к pi t t'.

LaTeX

$$$(hf : f \\in \\pi t t')(hg : g \\in \\pi t t') \\Rightarrow s.piecewise f g \\in \\pi t t'$$$

Lean4

theorem piecewise_mem_pi {δ : α → Type*} {t : Set α} {t' : ∀ i, Set (δ i)} {f g} (hf : f ∈ pi t t') (hg : g ∈ pi t t') :
    s.piecewise f g ∈ pi t t' := by
  intro i ht
  by_cases hs : i ∈ s <;> simp [hf i ht, hg i ht, hs]

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