mem_smul_set_iff_inv_smul_mem₀ — Mathlib

English

If a ≠ 0, then x ∈ a • A ↔ a⁻¹ • x ∈ A for any set A ⊆ β and x ∈ β; the inverse scalar maps back into A.

Русский

Если a ≠ 0, то x ∈ a • A ↔ a⁻¹ • x ∈ A для любого множества A ⊆ β и x ∈ β; обратный скаляр возвращает элемент в A.

LaTeX

$$$ (ha : a \neq 0) (A : Set β) (x : β), x \in a \cdot A \iff a^{-1} \cdot x \in A $$$

Lean4

theorem mem_smul_set_iff_inv_smul_mem₀ (ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A :=
  show _ ∈ Units.mk0 a ha • _ ↔ _ from mem_smul_set_iff_inv_smul_mem

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