English
If h1 and h2 are surjections onto t from s with h being injective on s ∪ s', then there is a surjection onto t from s ∩ s'.
Русский
Если имеем сюръекции на t от s1 и s2 c инъективностью на объединении, то существует сюръекция на t от пересечения s1 и s2.
LaTeX
$$$\\text{SurjOn } f\\ s_1\\ t \\land \\text{SurjOn } f\\ s_2\\ t \\land \\text{InjOn } f\\ (s_1 \\cup s_2) \\Rightarrow \\text{SurjOn } f\\ (s_1 \\cap s_2)\\ t.$$$
Lean4
theorem inter_inter (h₁ : SurjOn f s₁ t₁) (h₂ : SurjOn f s₂ t₂) (h : InjOn f (s₁ ∪ s₂)) :
SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂) := by
intro y hy
rcases h₁ hy.1 with ⟨x₁, hx₁, rfl⟩
rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩
obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm
exact mem_image_of_mem f ⟨hx₁, hx₂⟩
