smul_subset

Mathlib.Algebra.Order.UpperLower

URI: https://scilib.ai/kg/mathlib#IsUpperSet.smul_subset

English

If s is an upper set, then for any x ≥ 1, the scaled set x•s is contained in s.

Русский

Если s — верхнее множество, то при любом x ≥ 1 множество x•s ⊆ s.

LaTeX

$$$IsUpperSet(s) \rightarrow (1 \le x) \rightarrow x \cdot s \subseteq s$$$

Lean4

@[to_additive]
theorem smul_subset (hs : IsUpperSet s) (hx : 1 ≤ x) : x • s ⊆ s :=
  smul_set_subset_iff.2 fun _ ↦ hs <| le_mul_of_one_le_left' hx

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

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

Разделы

Аффилиация

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