piecewise_preimage — Mathlib

English

The preimage of a set t under the piecewise function s.piecewise f g is the piecewise preimage: s.piecewise f g)^{-1}(t) = s.ite (f^{-1}(t)) (g^{-1}(t)).

Русский

Образ множества t под(piecewise f g) задается как piecewise-предобразование: (s.piecewise f g)^{-1}(t) = s.ite (f^{-1}(t)) (g^{-1}(t)).

LaTeX

$$$(s.piecewise f g)^{-1}(t) = s.ite (f^{-1}(t)) (g^{-1}(t))$$$

Lean4

theorem piecewise_preimage (f g : α → β) (t) : s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t) :=
  ext fun x => by by_cases x ∈ s <;> simp [*, Set.ite]

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