smul_set_subset_smul_set_iff₀

Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

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

← MathLib Explorer

English

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

Русский

Если a ≠ 0, то a • A ⊆ B тогда и только тогда A ⊆ a⁻¹ • B.

LaTeX

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

Lean4

@[simp]
theorem smul_set_subset_smul_set_iff₀ (ha : a ≠ 0) {A B : Set β} : a • A ⊆ a • B ↔ A ⊆ B :=
  show Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_set_subset_smul_set_iff

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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