mem_smul_finset — Mathlib

English

Membership of an element in a scalar image is characterized by existence of a preimage: x ∈ a • s iff ∃ y ∈ s, a • y = x.

Русский

Членство элемента в образе скаляра характеризуется существованием предобраза: x ∈ a • s ⇔ ∃ y ∈ s, a • y = x.

LaTeX

$$$x \in a \cdot s \iff \exists y \in s, a \cdot y = x$$$

Lean4

@[to_additive]
theorem mem_smul_finset {x : β} : x ∈ a • s ↔ ∃ y, y ∈ s ∧ a • y = x := by simp only [Finset.smul_finset_def, mem_image]

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