smul_mem_pointwise_smul_iff₀ — Mathlib

English

Let a be a nonzero element acting on A, and S an additive submonoid of A. Then for every x ∈ A we have a · x ∈ a · S if and only if x ∈ S; i.e., the map x ↦ a · x induces a bijection between S and a · S when a ≠ 0.

Русский

Пусть a не равно нулю и действует на A, а S — аддитивный подмоноид A. Тогда для любого x ∈ A выполняется a · x ∈ a · S тогда и только тогда, когда x ∈ S; то есть отображение x ↦ a · x задаёт биекцию между S и a · S при a ≠ 0.

LaTeX

$$$\forall a\neq 0,\ \forall S:\text{AddSubmonoid } A,\ \forall x\in A: \ a\cdot x \in a\cdot S \iff x\in S.$$$

Lean4

@[simp]
theorem smul_mem_pointwise_smul_iff₀ (ha : a ≠ 0) (S : AddSubmonoid A) (x : A) : a • x ∈ a • S ↔ x ∈ S :=
  smul_mem_smul_set_iff₀ ha (S : Set A) x

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