smul_mem_nhds_smul_iff — Mathlib

English

For any t ⊆ α and g ∈ G, g · t ∈ nhds(g · a) iff t ∈ nhds(a).

Русский

Для любого t ⊆ α и g ∈ G, g · t ∈ nhds(g · a) тогда и только тогда, когда t ∈ nhds(a).

LaTeX

$$$g \cdot t \in \mathcal{N}(g \cdot a) \iff t \in \mathcal{N}(a)$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_mem_nhds_smul_iff {t : Set α} (g : G) {a : α} : g • t ∈ 𝓝 (g • a) ↔ t ∈ 𝓝 a :=
  (Homeomorph.smul g).isOpenEmbedding.image_mem_nhds

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