English
If f satisfies a certain injectivity-on-cross-pairs condition (∀ x∈t, ∀ y∈s, f(x) = f(y) ⇒ x = y), then the image of the intersection equals the intersection of the images: f''(s ∩ t) = f''s ∩ f''t.
Русский
Если f удовлетворяет условию инъективности на перекрёстках (∀ x∈t, ∀ y∈s, f(x) = f(y) ⇒ x = y), то образ пересечения равен пересечению образов: f''(s ∩ t) = f''s ∩ f''t.
LaTeX
$$$ (\\forall x \\in t)(\\forall y \\in s)(f(x) = f(y) \\Rightarrow x = y) \\Rightarrow f''(s \\cap t) = f''s \\cap f''t. $$$
Lean4
theorem image_inter_on {f : α → β} {s t : Set α} (h : ∀ x ∈ t, ∀ y ∈ s, f x = f y → x = y) :
f '' (s ∩ t) = f '' s ∩ f '' t :=
(image_inter_subset _ _ _).antisymm fun b ⟨⟨a₁, ha₁, h₁⟩, ⟨a₂, ha₂, h₂⟩⟩ ↦
have : a₂ = a₁ := h _ ha₂ _ ha₁ (by simp [*])
⟨a₁, ⟨ha₁, this ▸ ha₂⟩, h₁⟩
