smul_left

Mathlib.Topology.Algebra.ConstMulAction

URI: https://scilib.ai/kg/mathlib#IsOpen.smul_left

← MathLib Explorer

English

For any set s ⊆ G and t ⊆ α, if t is open then s · t is open in α.

Русский

Для любых множеств s ⊆ G и t ⊆ α, если t открыто, то s · t открыто в α.

LaTeX

$$$\text{IsOpen}(t) \Rightarrow \text{IsOpen}(s \cdot t)$$$

Lean4

@[to_additive]
theorem smul_left {s : Set G} {t : Set α} (ht : IsOpen t) : IsOpen (s • t) :=
  by
  rw [← iUnion_smul_set]
  exact isOpen_biUnion fun a _ => ht.smul _

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

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

Разделы

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

Аффилиация

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