div_closure

Mathlib.Topology.Algebra.Group.Pointwise

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

English

In a topological group, if s is open then s / closure(t) = s / t for any t.

Русский

В топологической группе, если s открыто, то s / closure(t) = s / t для любого t.

LaTeX

$$$\\forall S,T \\subseteq G,\\ (\\text{IsOpen}(S)) \\Rightarrow S / \\overline{T} = S / T$$$

Lean4

@[to_additive]
theorem div_closure (hs : IsOpen s) (t : Set G) : s / closure t = s / t := by
  simp_rw [div_eq_mul_inv, inv_closure, hs.mul_closure]

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

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

Разделы

Аффилиация

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