exists_smul_mem — Mathlib

English

For an IsMinimal action, given an open nonempty set U, there exists c ∈ M such that c•x ∈ U.

Русский

При минимальном действии существует элемент c ∈ M, приводящий x к открытой непустой подмножности U.

LaTeX

$$$\\exists c : M, c \\cdot x \\in U$$$

Lean4

@[to_additive]
theorem exists_smul_mem [IsMinimal M α] (x : α) {U : Set α} (hUo : IsOpen U) (hne : U.Nonempty) : ∃ c : M, c • x ∈ U :=
  (denseRange_smul M x).exists_mem_open hUo hne

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