image_inter — Mathlib

English

If f is injective on u and s ⊆ u and t ⊆ u, then f''(s ∩ t) = f''s ∩ f''t.

Русский

Если f инъективна на u и s ⊆ u, t ⊆ u, то образ пересечения равен пересечению образов.

LaTeX

$$$ \\operatorname{InjOn} f u \\land s \\subseteq u \\land t \\subseteq u \\Rightarrow f '' (s \\cap t) = f '' s \\cap f '' t$$$

Lean4

theorem image_inter {s t u : Set α} (hf : u.InjOn f) (hs : s ⊆ u) (ht : t ⊆ u) : f '' (s ∩ t) = f '' s ∩ f '' t :=
  by
  apply Subset.antisymm (image_inter_subset _ _ _)
  intro x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩
  have : y = z := by
    apply hf (hs ys) (ht zt)
    rwa [← hz] at hy
  rw [← this] at zt
  exact ⟨y, ⟨ys, zt⟩, hy⟩

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