inter_mul_singleton — Mathlib

English

Distributing left multiplication over intersection with a singleton: s ∩ t, when multiplied on the left by {a}, equals ({a} * s) ∩ ({a} * t).

Русский

Распределение умножения слева на пересечение с синглтоном: s ∩ t, умноженное слева на {a}, равно ({a} * s) ∩ ({a} * t).

LaTeX

$$$s \cap t * {a} = s * {a} \cap (t * {a})$$$

Lean4

@[to_additive]
theorem inter_mul_singleton (s t : Finset α) (a : α) : s ∩ t * { a } = s * { a } ∩ (t * { a }) :=
  image₂_inter_singleton _ _ <| mul_left_injective _

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