singleton_mul_inter — Mathlib

English

Multiplying a singleton on the left distributes over intersection: {a} * (s ∩ t) = ({a} * s) ∩ ({a} * t).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem singleton_mul_inter (a : α) (s t : Finset α) : { a } * (s ∩ t) = { a } * s ∩ ({ a } * t) :=
  image₂_singleton_inter _ _ <| mul_right_injective _

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