smul_subset_iff — Mathlib

English

For finite sets s, t, and u with a scalar action, s • t ⊆ u if and only if for every a in s and every b in t, a • b ∈ u.

Русский

Пусть s, t и u — конечные множества, на которые действует скаляр. Тогда s • t ⊆ u тогда и только тогда, когда для всех a ∈ s и b ∈ t выполняется a • b ∈ u.

LaTeX

$$$s \cdot t \subseteq u \iff \forall a \in s, \forall b \in t, a \cdot b \in u$$$

Lean4

@[to_additive]
theorem smul_subset_iff : s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u :=
  image₂_subset_iff

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