fst_mul_snd_subset — Mathlib

English

The product of the coordinates after applying the right transform is contained in the original product: (mulETransformRight e x).1 * (mulETransformRight e x).2 ⊆ x.1 * x.2.

Русский

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

LaTeX

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

Lean4

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

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