piecewise_mem_set_pi — Mathlib

English

If f and g belong to Set.pi t t' (i.e., are families of sections over t and t'), then s.piecewise f g also belongs to Set.pi t t'.

Русский

Если f и g являются элементами Set.pi t t' (семейства секций над t и t'), то s.piecewise f g тоже принадлежит Set.pi t t'.

LaTeX

$$$$f \\in \\mathrm{Set.pi}\\ t\\ t',\\; g \\in \\mathrm{Set.pi}\\ t\\ t' \\implies s.piecewise f g \\in \\mathrm{Set.pi}\\ t\\ t'. $$$$

Lean4

theorem piecewise_mem_set_pi (hf : f ∈ Set.pi t t') (hg : g ∈ Set.pi t t') : s.piecewise f g ∈ Set.pi t t' := by
  classical rw [← piecewise_coe]; exact Set.piecewise_mem_pi (↑s) hf hg

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