mem_inv_smul_set_iff₀ — Mathlib

English

If a ≠ 0, then x ∈ a⁻¹ • A ↔ a • x ∈ A, mirroring the previous relation with the inverse scalar.

Русский

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

LaTeX

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

Lean4

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

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