image_union_image_compl_eq_range — Mathlib

English

For any f: α → β and any subset s ⊆ α, the union of the image of s and the image of its complement equals the range of f.

Русский

Для любой функции f: α → β и любого подмножества s ⊆ α объединение образа s и образа множества дополнения s равно диапазону f.

LaTeX

$$$ f''s \\cup f''s^{c} = \\mathrm{range}(f). $$$

Lean4

@[simp]
theorem image_union_image_compl_eq_range (f : α → β) : f '' s ∪ f '' sᶜ = range f := by grind

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