subset — Mathlib

English

The Dyson e-transform of (S,T) with parameter e satisfies (S′,T′) ⊆ (S,T) under the natural product ordering, i.e., the product S′·T′ is contained in S·T.

Русский

Пусть (S,T) — пара подмножеств; преобразование Дайсона дает пару (S′,T′), удовлетворяющую S′·T′ ⊆ S·T.

LaTeX

$$(S′,T′) ⊆ (S,T)$$

Lean4

@[to_additive]
theorem subset : (mulDysonETransform e x).1 * (mulDysonETransform e x).2 ⊆ x.1 * x.2 :=
  by
  refine union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)
  rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]

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