smul_set_subset_smul_set_iff — Mathlib

English

For A,B ⊆ β and a ∈ α, a • A ⊆ a • B if and only if A ⊆ B (via injectivity of the action).

Русский

Для подмножеств A,B ⊆ β и элемента a ∈ α верно: a•A ⊆ a•B тогда и только тогда, когда A ⊆ B (через инъективность действия).

LaTeX

$$$\forall A,B\subseteq β:\ a\cdot A \subseteq a\cdot B \iff A\subseteq a^{-1}\cdot B.$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_set_subset_smul_set_iff : a • A ⊆ a • B ↔ A ⊆ B :=
  image_subset_image_iff <| MulAction.injective _

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