smul_set_mem_smul_filter

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.smul_set_mem_smul_filter

English

If s ∈ f, then a • s ∈ a • f.

Русский

Если s ∈ f, то a • s ∈ a • f.

LaTeX

$$$ s \in f \Rightarrow a \cdot s \in a \cdot f$$$

Lean4

@[to_additive]
theorem smul_set_mem_smul_filter : s ∈ f → a • s ∈ a • f :=
  image_mem_map

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

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

Разделы

Аффилиация

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