fst_mul_snd_subset — Mathlib

English

Applying the left energy transform to x produces a pair whose product of components is a subset of the product of x’s components: (mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2.

Русский

Применение левого преобразования энергии к x даёт пару, у которой произведение двух компонент является подмножество произведения компонент x: (mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2.

LaTeX

$$$ (\\mathrm{mulETransformLeft}\\, e\\, x).1 \\cdot (\\mathrm{mulETransformLeft}\\, e\\, x).2 \\subseteq x.1 \\cdot x.2 $$$

Lean4

@[to_additive]
theorem fst_mul_snd_subset : (mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2 :=
  by
  refine inter_mul_union_subset_union.trans (union_subset Subset.rfl ?_)
  rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]

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