English
Let S be a nontrivial subgroup of a archimedean linearly ordered multiplicative group G with order topology. If the set of elements of S greater than 1 has no least element, then S is dense in G.
Русский
Пусть S — не тривиальная подгруппа в упорядоченной группе G; если множество элементов S, больших 1, не имеет наименьшего элемента, тогда S плотно внутри G.
LaTeX
$$dense_of_not_isolated_one(S, hS) : Dense(S)$$
Lean4
/-- Let `S` be a nontrivial subgroup in an archimedean linear ordered multiplicative commutative
group `G` with order topology. If the set of elements of `S` that are greater than one
does not have a minimal element, then `S` is dense `G`. -/
@[to_additive /-- Let `S` be a nontrivial additive subgroup in an archimedean linear ordered
additive commutative group `G` with order topology. If the set of positive elements of `S` does not
have a minimal element, then `S` is dense `G`. -/
]
theorem dense_of_no_min (S : Subgroup G) (hbot : S ≠ ⊥) (H : ¬∃ a : G, IsLeast {g : G | g ∈ S ∧ 1 < g} a) :
Dense (S : Set G) := by
refine S.dense_of_not_isolated_one fun ε ε1 => ?_
contrapose! H
exact exists_isLeast_one_lt hbot ε1 (disjoint_left.2 H)
