instMulRightMono — Mathlib

English

Let Finset α be with pointwise multiplication. For Finsets s, t, t' with t ⊆ t', we have s * t ⊆ s * t'. Thus right multiplication by a fixed Finset is monotone with respect to inclusion.

Русский

Пусть Finset α оснащено покомпонентным умножением. Для конечных множеств s, t, t' верно: если t ⊆ t', тогда s * t ⊆ s * t'. Это правое умножение сохраняет включение.

LaTeX

$$$t \\subseteq t' \\Rightarrow s * t \\subseteq s * t'$$$

Lean4

@[to_additive]
instance : MulRightMono (Finset α) where elim _t _s₁ _s₂ := mul_subset_mul_right

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