English
Let h ∘ f = f₁ ∘ f₂ and h ∘ g = g₁ ∘ g₂ with hfg: range f ∪ range g = univ. Then for any s ⊆ β, the image h''s equals the union of the two corresponding images: h''s = f₁''(f₂''(f⁻¹s)) ∪ g₁''(g₂''(g⁻¹s)).
Русский
Пусть выполняются равенства h ∘ f = f₁ ∘ f₂ и h ∘ g = g₁ ∘ g₂, а также покрытие диапазонов hfg: range f ∪ range g = univ. Тогда для любого s ⊆ β выполняется разложение изображения: h''s = f₁''(f₂''(f⁻¹s)) ∪ g₁''(g₂''(g⁻¹s)).
LaTeX
$$$\forall s \subseteq \beta,\; h'' s = f_1''(f_2''(f^{-1} s)) \cup g_1''(g_2''(g^{-1} s)) \quad\text{при } hf : h \circ f = f_1 \circ f_2,\; hg : h \circ g = g_1 \circ g_2,\; hfg : \operatorname{range} f \cup \operatorname{range} g = \operatorname{univ}.$$$
Lean4
theorem image_of_range_union_range_eq_univ {α β γ γ' δ δ' : Type*} {h : β → α} {f : γ → β} {f₁ : γ' → α} {f₂ : γ → γ'}
{g : δ → β} {g₁ : δ' → α} {g₂ : δ → δ'} (hf : h ∘ f = f₁ ∘ f₂) (hg : h ∘ g = g₁ ∘ g₂)
(hfg : range f ∪ range g = univ) (s : Set β) : h '' s = f₁ '' (f₂ '' (f ⁻¹' s)) ∪ g₁ '' (g₂ '' (g ⁻¹' s)) := by
rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
