subset_smul_set_iff₀

Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

URI: https://scilib.ai/kg/mathlib#Set.subset_smul_set_iff₀

English

If a ≠ 0, then A ⊆ a • B iff a⁻¹ • A ⊆ B (equivalently A ⊆ a⁻¹ • B).

Русский

Если a ≠ 0, то A ⊆ a • B эквивалентно a⁻¹ • A ⊆ B.

LaTeX

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

Lean4

theorem subset_smul_set_iff₀ (ha : a ≠ 0) {A B : Set β} : A ⊆ a • B ↔ a⁻¹ • A ⊆ B :=
  show _ ⊆ Units.mk0 a ha • _ ↔ _ from subset_smul_set_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru