instMulLeftMono — Mathlib

English

Let Finset α carry the pointwise multiplication. For Finsets s, s′, t ⊆ α, if s ⊆ s′ then s * t ⊆ s′ * t for every t. In words, left multiplication by a fixed Finset is monotone with respect to inclusion.

Русский

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

LaTeX

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

Lean4

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

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