image_inter — Mathlib

English

If f is injective, then the image of the intersection equals the intersection of the images: f''(s ∩ t) = f''s ∩ f''t.

Русский

Если f инъективно, то образ пересечения равен пересечению образов: f''(s ∩ t) = f''s ∩ f''t.

LaTeX

$$$ \\text{Injective}(f) \\Rightarrow f''(s \\cap t) = f''s \\cap f''t. $$$

Lean4

theorem image_inter {f : α → β} {s t : Set α} (H : Injective f) : f '' (s ∩ t) = f '' s ∩ f '' t :=
  image_inter_on fun _ _ _ _ h => H h

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