iUnion_smul — Mathlib

English

Let G act on α with a minimal action. If U is an open nonempty subset of α, then the union of all translates g · U (as g runs over G) equals the whole space α.

Русский

Пусть G действует на α минимальным образом. Пусть U ⊆ α открыто и не пусто. Тогда ⋃_{g∈G} g·U = α.

LaTeX

$$$$\bigcup_{g \in G} g \cdot U = \text{univ}$$$$

Lean4

@[to_additive]
theorem iUnion_smul [IsMinimal G α] {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) : ⋃ g : G, g • U = univ :=
  iUnion_eq_univ_iff.2 fun x ↦
    let ⟨g, hg⟩ := hUo.exists_smul_mem G x hne
    ⟨g⁻¹, _, hg, inv_smul_smul _ _⟩

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