mul_subset_iff_right

Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.mul_subset_iff_right

English

s * t ⊆ u iff for all b ∈ t, op b · s ⊆ u.

Русский

s * t ⊆ u эквивалентно: для каждого b ∈ t, op b · s ⊆ u.

LaTeX

$$$ s * t \subseteq u \iff \forall b \in t, \mathrm{op} b \cdot s \subseteq u $$$

Lean4

@[to_additive]
theorem mul_subset_iff_right : s * t ⊆ u ↔ ∀ b ∈ t, op b • s ⊆ u :=
  image2_subset_iff_right

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru