range_piecewise — Mathlib

English

The range of the piecewise function s.piecewise f g is the union of the image of f on s and the image of g on sᶜ.

Русский

Образ кусочно-заданной функции s.piecewise f g равен объединению образов f на s и g на sᶜ.

LaTeX

$$$\\operatorname{range}(s.piecewise f g) = f''s \\cup g''s^{c}$$$

Lean4

theorem range_piecewise (f g : α → β) : range (s.piecewise f g) = f '' s ∪ g '' sᶜ :=
  by
  ext y; constructor
  · rintro ⟨x, rfl⟩
    by_cases h : x ∈ s <;> [left; right] <;> use x <;> simp [h]
  · rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩) <;> use x <;> simp_all

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