smul_finset_snd_subset_fst — Mathlib

English

For any nonzero scalar e, the scaled second component of the Dyson transform is contained in the first component: e • (mulDysonETransform e x).2 ⊆ (mulDysonETransform e x).1.

Русский

Для любого ненулевого скаляра e, домножение второй компоненты на e вложено в первую: e•(mulDysonETransform e x)₂ ⊆ (mulDysonETransform e x)₁.

LaTeX

$$e \\cdot (mulDysonETransform e x).2 \\subseteq (mulDysonETransform e x).1$$

Lean4

@[to_additive]
theorem smul_finset_snd_subset_fst : e • (mulDysonETransform e x).2 ⊆ (mulDysonETransform e x).1 :=
  by
  dsimp
  rw [smul_finset_inter, smul_inv_smul, inter_comm]
  exact inter_subset_union

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