pointwise_smul_le_pointwise_smul_iff₀

English

If a ≠ 0, then the map S ↦ a · S preserves inclusion: a · S ≤ a · T if and only if S ≤ T.

Русский

Если a ≠ 0, то отображение S ↦ a · S сохраняет включение: a · S ⊆ a · T тогда и только тогда, когда S ⊆ T.

LaTeX

$$$\forall a\neq 0:\ a\cdot S \le a\cdot T \iff S \le T$.$$

Lean4

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff₀ (ha : a ≠ 0) : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff₀ ha

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