image_inter_subset — Mathlib

English

The image of an intersection is contained in the intersection of the images: f''(s ∩ t) ⊆ f''s ∩ f''t.

Русский

Образ пересечения содержится в пересечении образов: f''(s ∩ t) ⊆ f''s ∩ f''t.

LaTeX

$$$ f''(s \\cap t) \\subseteq f''s \\cap f''t. $$$

Lean4

theorem image_inter_subset (f : α → β) (s t : Set α) : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
  subset_inter (image_mono inter_subset_left) (image_mono inter_subset_right)

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