iUnion_preimage_smul — Mathlib

English

For an IsMinimal action, the union over c ∈ M of the preimages under c• of an open nonempty set U equals the whole space.

Русский

Для минимального действия объединение по всем c ∈ M предобразов под c• открытого непустого множества U равно всей пространству.

LaTeX

$$$\\\\bigcup_{c \\in M} (c \\cdot)^{-1}(U) = \\text{univ}.$$$

Lean4

@[to_additive]
theorem iUnion_preimage_smul [IsMinimal M α] {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) :
    ⋃ c : M, (c • ·) ⁻¹' U = univ :=
  iUnion_eq_univ_iff.2 fun x ↦ hUo.exists_smul_mem M x hne

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