image_inter_subset — Mathlib

English

For any R and sets s1, s2, the image of their intersection equals the intersection of their images: image R (s1 ∩ s2) = image R s1 ∩ image R s2.

Русский

Образ пересечения подмножеств равен пересечению образов: image R (s1 ∩ s2) = image R s1 ∩ image R s2.

LaTeX

$$$\\forall (R : SetRel \\alpha \\beta) (s1 s2 : Set \\alpha),\\\\ image\\,R\\,(s1 \\cap s2) = image\\,R\\,s1 \\cap image\\,R\\,s2$$$

Lean4

theorem image_inter_subset : image R (s₁ ∩ s₂) ⊆ image R s₁ ∩ image R s₂ :=
  image_mono.map_inf_le ..

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