mapClusterPt_inv_atTop_pow — Mathlib

English

The equivalence MapClusterPt x^{-1} atTop (y^·) ↔ MapClusterPt x atTop (y^·) holds for all x,y ∈ G.

Русский

Справедливо равенство: MapClusterPt x^{-1} atTop (y^·) ⇔ MapClusterPt x atTop (y^·) для всех x,y ∈ G.

LaTeX

$$$\text{MapClusterPt}(x^{-1},\mathrm{atTop}, y^{\cdot}) \iff \text{MapClusterPt}(x,\mathrm{atTop}, y^{\cdot}).$$$

Lean4

@[to_additive (attr := simp)]
theorem mapClusterPt_inv_atTop_pow {x y : G} :
    MapClusterPt x⁻¹ atTop (y ^ · : ℕ → G) ↔ MapClusterPt x atTop (y ^ · : ℕ → G) := by
  simp only [mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers, inv_mem_iff]

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