mul_inter_subset — Mathlib

English

The product with an intersection on the right is contained in the intersection of the products: s * (t1 ∩ t2) ⊆ (s * t1) ∩ (s * t2).

Русский

Произведение с пересечением слева по отношению к правому аргументу: s * (t1 ∩ t2) ⊆ (s * t1) ∩ (s * t2).

LaTeX

$$s * (t_1 \\cap t_2) \\subseteq s * t_1 \\cap (s * t_2)$$

Lean4

@[to_additive]
theorem mul_inter_subset : s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂) :=
  image₂_inter_subset_right

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