preimage_inter_subset — Mathlib

English

For any R and sets t1, t2, the preimage of their intersection is contained in the intersection of their preimages: preimage R (t1 ∩ t2) ⊆ preimage R t1 ∩ preimage R t2.

Русский

Предобраз пересечения содержится в пересечении предобразов: preimage R (t1 ∩ t2) ⊆ preimage R t1 ∩ preimage R t2.

LaTeX

$$$\\forall (R : SetRel \\alpha \\beta) (t1 t2 : Set \\beta),\\\\ preimage\\,R\\,(t1 \\cap t2) \\subseteq preimage\\,R\\,t1 \\cap preimage\\,R\\,t2$$$

Lean4

theorem preimage_inter_subset : preimage R (t₁ ∩ t₂) ⊆ preimage R t₁ ∩ preimage R t₂ :=
  preimage_mono.map_inf_le ..

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