image_inter — Mathlib

English

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

Русский

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

LaTeX

$$$f.image\\,(s \\cap t) \\subseteq f.image\\,s \\cap f.image\\,t$$$

Lean4

theorem image_inter (s t : Set α) : f.image (s ∩ t) ⊆ f.image s ∩ f.image t :=
  SetRel.image_inter_subset _

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